Formal verification has nothing to do with the quality of the API.

Given the spec, formal verification can tell you if your implementation follows the spec. It cannot tell you if the spec if good

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.

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

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!)

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".

> Formal verification will eventually lead to good, stable API design.

Why? Has it ever happened like this? Because to me it would seem that if the system verified to work, then it works no matter how API is shaped, so there is no incentive to change it to something better.

> if the system verified to work, then it works no matter how API is shaped

That's the case for one-off integrations, but the messy part always comes when system goal changes

Let's say formal verification could help to avoid some anti-patterns.

> Let's say formal verification could help to avoid some anti-patterns.

I'd still like to hear about the actual mechanism of this happening. Because I personally find it much easier to believe that the moment keeping the formal verification up to date becomes untenable for whatever reason (specs changing too fast, external APIs to use are too baroque, etc) people would rather say "okay, guess we ditch the formal verification and just keep maintaining the integration tests" instead of "let's change everything about the external world so we could keep our methodology".

> I'd still like to hear about the actual mechanism of this happening

I am not an expert on this, but the worst API I've seen is those with hidden states.

e.g. .toggle() API. Call it old number of times, it goes to one state, call it even number of times, it goes back.

And there's call A before you call B types of APIs, the client has to keep a strict call order (which itself is a state machine of some kind)

> I am not an expert on this, but the worst API I've seen is those with hidden states.

> e.g. .toggle() API. Call it old number of times, it goes to one state, call it even number of times, it goes back.

This is literally a dumb light switch. If you have trouble proving that, starting from lights off, flicking a simple switch twice will still keep lights off then, well, I have bad news to tell you about the feasibility of using the formal methods for anything more complex than a dumb light switch. Because the rest of the world is a very complex and stateful place.

> (which itself is a state machine of some kind)

Yes? That's pretty much the raison d'être of the formal methods: for anything pure and immutable, normal intuition is usually more than enough; it's tracking the paths through enormous configuration spaces that our intuition has problem with. If the formal methods can't help with that with comparable amount of effort, then they are just not worth it.

Isn’t this where the Eiffel design by contract people speak up about code reuse?

At that point you create an entirely new API, fully versioned, and backwardly compatible (if you want it to be). The point the article is making is that AI, in theory, entirely removes the person from the coding process so there's no longer any need to maintain software. You can just make the part you're changing from scratch every time because the cost of writing bug-free code (effectively) goes to zero.

The theory is entirely correct. If a machine can write provably perfect code there is absolutely no reason to have people write code. The problem is that the 'If' is so big it can be seen from space.

100% of state changes in business software is unknowable on a long horizon, and relies on thoroughly understanding business logic that is often fuzzy, not discrete and certain.

Formal verification does not gurantee business logic works as everybody expected, nor its future proof, however, it does provide a workable path towards:

Things can only happen if only you allow it to happen.

It other words, your software may come to a stage where it's no longer applicable, but it never crashes.

Formal verification had little adoption only because it costs 23x of your original code with "PhD-level training"

The reason it doesn't work is businesses change faster than you can model every detail AND keep it all up to date. Unless you have something tying your model directly to every business decision and transaction that happens, your model will never be accurate. And if we're talking about formal verification, that makes it useless.