> And the separation between the spec and the "proof" bothers me: what is the point of a spec if, after building a product, you can't verify you built it right?

> And the separation between the spec and the "proof" bothers me: what is the point of a spec if, after building a product, you can't verify you built it right? I would consider such specs as incomplete. You have a spec, that says what the code should do. This is independent of the code; there can be many ways to write the code to match a given spec. You have a proof, that says what the code does do. This is intimately tied to the code, and with the right languages and tools can be the code. You verify that you built it right, by seeing that they match. This is abstraction, the basic interface/implementation distinction; the spec is an interface and the code+proof is an implementation.