Benchmarking Crimes Meet Formal Verification

Sigh.

Decades ago I headed a project to build a proof of correctness system.[1] It was for a rather dialect of Pascal for real-time engine control programs. Some of the comments I made back then still apply.

- Assertions belong in the program source, and in the same syntax as the language of the program. They're mostly written by the people writing the code. The proof of correctness work can and should be integrated with development.

- Most, but not all, of the theorem proving can be automated with what's now called a "SAT solver". We had the original Oppen-Nelson simplifier for that.

- Sometimes you need more theorem proving power than a SAT solver. We used the original Boyer-Moore theorem prover for that. It's automatic, but you can help it by suggesting intermediate theorems.

- To tie complex theorems to concrete code, programmers should write

    assert(a);
    assert(b);

where a can be proved from the code above by the SAT solver, and b is what you need to prove constraints on the following code. Now you have to prove a implies b. That's when you need a more interactive prover, or one with more power. a implies b should be a statement that stands alone, without reference to other code. This allows turning the problem over to the people who are into theorem proving, while the programmers can get on with coding.

- Many of the people involved in program verification are heavily into the formalism, rather than seeing this as a way to eliminate bugs. This leads to excessive formalism. That tendency has to be restrained.

[1] https://github.com/John-Nagle/pasv