> I think this sharply discounts the value of the step before the proof which is writing the specification in a formal language/logic.
If that was at all achievable, we'd have a compiler that took the "specification in a formal language/logic" and emitted native code/applications/programs. We'd then call the "specification in a formal language/logic" a programming language.
Sure, there are a lot of formal languages for specifying logic with checkers that ensure no bugs in the input specification exist, but AFAIK none of them are useful enough to emit programs.
Needing a human to translate one formal language (the formal spec) into another formal language is pointless and useless, because then the human may as well just translate human language specification into formal language.
If you're writing a sorting algorithm or a hash table implementation or something, then the spec is meaningfully different from the code. The spec says "the output array is sorted", the program describes some particular strategy for sorting it, and then you use the proof tools to make sure that the strategy actually works to sort the array in all cases.
But for things like UI code, I too am having trouble imagining a spec that is concrete enough to be useful for formal verification and does not have some trivial 1:1 correspondence to the implementation. (If anyone knows of an example, I'd really be interested in seeing it!)
> If you're writing a sorting algorithm or a hash table implementation or something, then the spec is meaningfully different from the code. The spec says "the output array is sorted", the program describes some particular strategy for sorting it, and then you use the proof tools to make sure that the strategy actually works to sort the array in all cases.
I dunno. Thinking more deeply about the specification for a sorting algorithm, it makes sense that the specification includes the O(n) runtime (or memory usage, or both), or else it's an informal specification.
If the spec is really nailed down formally then the specification language really would be the implementation language too.
If that was at all achievable, we'd have a compiler that took the "specification in a formal language/logic" and emitted native code/applications/programs. We'd then call the "specification in a formal language/logic" a programming language.
Sure, there are a lot of formal languages for specifying logic with checkers that ensure no bugs in the input specification exist, but AFAIK none of them are useful enough to emit programs.
Needing a human to translate one formal language (the formal spec) into another formal language is pointless and useless, because then the human may as well just translate human language specification into formal language.