3 ms·
>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 sho
by ivanbakel 2mo ago
>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.
- makeitdouble 2mo ago> 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.
- deterministic 2mo agoThe trick is to start with the smallest possible implementation of a spec and proving it correct. You then add a more advanced and faster implementation and prove that the 2nd implementation implements the 1st. Etc. etc. It's called refinement and it's a great way to prove really complex software correct. You basically have a formally proven correct chain of software from simple to advanced. CompCert is an example of how to do this.
- Veserv 2mo agoHuh? 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.
- inigyou 2mo agoThe trivial sorting spec is actually very useful, it's just not complete. While knowing that your sorting program meets the complete spec proves it works correctly, if you wrote it intending to be a sort algorithm, and you have proven it meets the trivial spec, and you have a few unit tests, that's still very good-but-not-foolproof evidence it's correct.
- pastel8739 2mo agodo you have a reference to anywhere that discusses this further? It seems pretty trivial to me
- inigyou 2mo agoYou 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?
- pastel8739 2mo agoOk, I’ll bite, why is this wrong? For a list of items I and an operator LEQ which returns bool for any pair of items in I, SORT() returns a list S such that: 1. Every item in I is present exactly once in S 2. For each consecutive pair of items (S_i, S_j) in S, LEQ(S_i, S_j) is true.
- inigyou 2mo agoSORT(1,2,3,4,5,5,6) = 1,2,3,4,5,6
- defrost 2mo agoI'm sorry, do all 5's look the same to you!! /s aka, one item in I is missing in your output.
- inigyou 2mo agoNo, if it had one more 5 it would violate your specification that every time must occur exactly once. Also, SORT(1,2,3,4) = 1,2,3,4,7
- defrost 2mo agoNot my specification (drive by third party) but I do take the view that ( 1, 2, 3, 4, 5, 5, 6 ) is a list of seven values (perhaps the number of dollars in the pockets of seven distinct unique people) and when sorted the output should also have seven items that correspond to the seven input items. > Also ... Yeah, that needs tightening up by pastel8739