Thats something I agree with.

I am right now working on an offline api client: https://voiden.md/. I wonder if this can be a feature.

> It cannot tell you if the spec if good

I beg to differ, if a spec is hard to verify, then it's a bad sign.

All non-trivial specs, like the one for seL4, are hard to verify. Lots of that complexity comes from interacting with the rest of the world which is a huge shared mutable global state you can't afford to ignore.

Of course, you can declare that the world itself is inherently sinful and imperfect, and is not ready for your beautiful theories but seriously.

> Of course, you can declare that the world itself is inherently sinful and imperfect, and is not ready for your beautiful theories

i see we are both familiar with haskellers (friendly joke!)

it can tell you if your spec is bad, but it can't tell you if your spec is good

That is one problem of many solved, isn't that good?

That the spec solves the problem is called validation in my domain and treated explicitly with different methods.

We use formal validation to check for invariants, but also "it must return a value xor an error, but never just hang".