About the Analogy between Verification and Compilation

Some people in the verification community have started responding to the complaint that formal proofs of program correctness are too long by making an analogy between verifiers and compilers:

Formal proofs of correctness are tedious in the same way coding in assembler is tedius. The use of tools, namely high level programming languages, solved the latter, and it can also solve the former.

I've seen it many times and I don't really know whom to credit for it. I think the analogy is fundamentally flawed. For one thing, the translation of high level programming language into assembler is a computable problem and its use is rather straightforward if the language is well designed and its semantics is as simple and systematic as it can be. We don't have any such luck with automated theorem provers. Since their job is to solve an uncomputable problem, they have to use lots of heuristics which make the interface with the user fuzzy. When submitting formula to the theorem prover, there is no way of saying if it will be found to be a theorem or not because the class of recognized theorems is not precisely defined. On the other hand, given a theorem (in our case the conformance of a given program to a given specification) the problem of generating a proof is well know to be uncomputable. But this should not deter us in seeking a formal backing for our design because, contrary to the folklore, writing a formal proof is not a tedious activity. It is hard but it is a very inventive process. It can become tedious though if one uses an inappropriate logic like, say Gentzen's Natural Deduction or like the sequent calculus. Although they are popular formal logic system, they are hardly the only ones available. It is not too say that they are useless formal systems, just like Turing Machines are not useless. They are not meant to be used but meant as a simplification for logicians and theoreticians to understand what tasks can be accomplished with the formal system. It is not proper for understanding how best to accomplish the tasks. Just like programming directly with Turing machines is a waste of effort, proving with Natural Deduction is also a waste of effort. It forces the user of making irrelevant distinctions, for example, with its rule for the proof of logical equivalence. The only way to prove it or even to use it is as a shorthand for two implications. Very often, you can exploit properties of logical equivalence in the calculations of theorems (like it is done in [0] and [1]) in at most half of the effort (and some times one fourth or less) that would be expended for the same proof in Natural Deduction. Contrarily to Natural Deduction, the use of calculational proofs allows one to focus on the subject matter and use the activity of proving as an improvement of his understanding rather than as a necessary evil for being certain of one's guesses. As a consequence, automating the construction of the significant proofs of correctness does not improve the productivity but decreases it because it removes any useful hints that the (human) prover could use to orient his efforts in the right direction. In short, in all important respect, the analogy is invalid and cannot be used to the defend the necessity of automating theorem proving. It is so first because, of the two compared activities, only one solves a computable problem, and, second, one of them is tedious and repetitive whereas the other involves a lot creativity. The fallacy comes from talking some properties of inappropriate formal systems as being valid for all of them. To be effective at proving, we don't only need a logic which is sound and theoretically powerful enough, we need a formalism suited as a carrier for reasoning. References [0] On the Shape of Mathematical Arguments, A.J.M. van Gasteren [1] Predicate Calculus and Program Semantics, E.W. Dijkstra and C.S. Scholten