Casual Attire and Formal Proof
BLOG: Heidelberg Laureate Forum
Informality is the watchword here at the Heidelberg Laureate Forum. Even the most distinguished participants go by Bob or Fred or Len rather than Herr Professor Doktor. In this casual social atmosphere, however, formality of another kind has been a major topic of conversation. Four of the week’s plenary lectures have addressed the need for formal proofs of correctness in both computer science and mathematics.
Tony Hoare gave an eloquent talk reclaiming two giants of Greek antiquity as part of the tradition of computer science. The logical syllogisms of Aristotle and the geometrical theorems of Euclid are statements whose correctness can be verified by purely mechanical means. In these realms truth depends only on the axioms and the grammatical form of the propositions, not on the reader’s interpretations. Hoare has long argued that computer programs deserve an analogous proof of correctness. In his 1969 paper “An Axiomatic Basis for Computer Programming,” he wrote:
The practice of supplying proofs for nontrivial programs will not become widespread until considerably more powerful proof techniques become available, and even then will not be easy. But the practical advantages of program proving will eventually outweigh the difficulties, in view of the increasing costs of programming error.
At the end of his talk, Hoare observed that he has been able to continue in the same line of research throughout his career because his recommendation has still not been taken up by most of the software industry.
Leslie Lamport addressed a similar theme, proposing to apply formal proof techniques not to programs themselves but to the specifications that prescribe their behavior. Lamport would harness some of the notation and conceptual foundations of mathematics to this purpose. A computer system can be viewed as a mechanism that has a finite number of possible states, along with a set of allowed transitions between states. The simplest example of such a system might be an oscillator that periodically shifts from off to on and back to off again. Rather than try to catalogue all possible behaviors of such a system, the mathematical approach describes the initial state and supplies a relation between successive states that can be proved to hold in all future evolutions of the system.
Lamport has developed a specification language, TLA+ (TLA stands for Temporal Logic of Actions) that facilitates writing such verifiable specifications. “It’s not a toy language,” Lamport says. It has been put to use by Intel and Amazon, and also in the operating system of the Rosetta spacecraft, now orbiting comet 67P/Churyumov–Gerasimenko.
Edmund Clark discussed the latest applications of the model-checking methodology for which he received the Turing Award in 2007. The current challenge is to verify correctness in “hybrid” systems, which combine components with discrete states and those that vary over a continuous range of values. An example is the controller for a self-driving automobile; the selection of forward or reverse gear is a discrete variable, whereas velocity is a continuous one.
The analysis of these systems is so complex that strict mathematical rigor is an unrealistic goal. The task must be formulated as an optimization problem, some parts of which are then solved by numerical approximation. On the other hand, the approximation can be made arbitrarily accurate, and the remaining error can be quantified.
Vladimir Voevodsky spoke not on applying mathematical reasoning to ensure the correctness of computer software but on developing software to certify the correctness of mathematics. Voevodsky and his colleagues are building an open-source software framework called UniMath that will apply rigorous standards of proof checking to theorems already in the mathematical literature and also provide a tool for mathematicians who want to verify their own proofs prior to publication. Toward that end Voevodsky has adopted a new mode of discourse in his own mathematical writing, giving all proofs in full even if they seem obvious or trivial.
Voevodsky’s vision for the future of mathematics is rather like Hoare’s for the future of software engineering: All published work will be formally and mechanically verified. A further question remains unanswered: Is this yearning for rigor and certainty shared by the younger generation of computer scientists and mathematicians?