[Ygg2]

> "Formal verification" literally means that the implementation is proven to satisfy the formal specification, so by definition there won't be any gaps.

To quote Donald Knuth:

    "Beware of bugs in the above code; I have only proved it correct, not tried it."

Sure but proof itself might have gaps itself. A famous proved implementation of mergesort had a subtle flaw when array size approached usize. They proved it would sort, they didn't prove it won't experience UB. Or maybe you prove it has no UB if there are no hardware errors (there are hardware errors), etc.

The unbeatable quantum cryptography was beat in one instance because the attacker abused the properties of detectors to get the signal without alerting either sides of the conversation.

https://www.theregister.com/2010/09/01/quantum_crypto_hack/

> Or maybe you mean "specification" to be some kind of informal description?

I read somewhere that the secret to hacker mindset is that they ignore what the model is, but look at what is actually there. If they behaved as spec writers expected, they would have never been able to break in.

Reminds me of a place I worked. The doors were this heavy mass of wood and metal that would unlock with a loud thud (from several huge rods holding it secure). This was done to formally pass some ISO declaration for document security. The thing is any sane robber would just easily bypass the door by breaking the plaster walls on either side.

At least we can stop writing code made of plaster for start.

[yusina]

> Sure but proof itself might have gaps itself.

Then it's an incorrect proof. In the pen-and-paper era, that was a thing, but nowadays proofs are machine-checked and don't have "gaps" anymore.

Or your assumptions have a bug. That's exactly what I mean with specifications being potentially flawed, since all assumptions must be baked into the formal specification. If hardware can fail then that must be specified, otherwise it's assumed to not fail ever. This never ends, and that's the whole point here.

I suppose we are trying to say the same thing, just not with the same terminology.