[csande17]

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

[lelanthran]

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