alt Hacker News>why would the formal verification be any more correct than the program it is verifying?
It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result - especially in the most common settings targeted by verification, which is to say imperative, stateful programs or algortihms with a high degree of non-obvious optimisations. The simplest example is a sorting algorithm, which normally has a trivial spec but a non-trivial state at each step.
Interestingly, some specs are actually programs themselves, as has also been true for many on-paper specs which are actually reference implementations. Research using programs-as-specs is still pretty valuable, since in some domains a simpler program is actually the right and useful way to talk about a messier one.
Replies
> It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result
This is obvious for the central cases of a program. It becomes less and less true when going toward the edge cases, especially for a wide array of input.
Complex specs becoming programs is IMHO the direct effect of that (defining what we want is just that burdensome, and special cases we haven't though of will still have a coherent definition in the spec), and we fall back to the base "is this spec even correct" issue the parent points out.
Huh? Sorting does not have a trivial specification. In fact, it is usually used as the first example of how easy it is to make specification errors because it seems trivial, but is actually not.
You know, the last time someone brought up formal verification of sorting I said what the trivial spec was, and then someone else pointed out why it's actually completely wrong.
So for pedagogical purposes, can you tell us what you think the trivial spec is?