1969 United Kingdom meta

An Axiomatic Basis for Computer Programming

Tony Hoare, 1969 — programs can be reasoned about with mathematical precision. The first technique that makes maintenance survivable.

Tony Hoare, then at the Queen's University of Belfast, published a system of inference rules for proving the correctness of computer programs. The central object is the Hoare triple: a precondition, a program fragment, and a postcondition, denoted {P} S {Q}. The triple asserts that if P holds before S runs, then Q holds after. Hoare gave axioms for assignment, sequencing, conditionals, and loops, with a separate rule for each. Together these rules let a programmer construct a proof, alongside the code, that the code does what it claims. This is the technical foundation of every later formal-methods system in this book — Dijkstra's weakest preconditions, separation logic, SPARK, Coq, Isabelle, Dafny, the proofs of seL4 and CompCert. It is the only technique humans have invented that beats Rice's theorem on a per-program basis.

In plain terms

Rice's theorem says no general-purpose tool can decide whether an arbitrary program is correct. Hoare did not contradict Rice — he sidestepped him. His insight was that you do not need a general-purpose tool that works for any program. You need a system in which a programmer can construct a specific proof for a specific program. The proof goes alongside the code, and the proof is checked mechanically. The shape of a Hoare proof is the triple — three pieces, written in a row. The thing that must be true before this code runs. The code itself. The thing that must be true after. Hoare gave you the rules for combining triples. If you want to prove a sequence of two statements, you prove a triple for each and chain them at the middle assertion. If you want to prove a loop, you find an invariant — a statement that is true before the loop, true after every iteration, and that combined with the loop's exit condition gives you the postcondition. Loop invariants are hard. They are the heart of programming as a discipline. This is the first technique in the book that beats undecidability on a per-program basis. Rice's theorem still holds: there is no algorithm that proves an arbitrary program correct. But there is a language in which a human can construct a proof, and a checker that verifies the proof is valid. This is the key that opens every door later in the book. When you read about CompCert proving a C compiler correct, the proof is in a descendant of Hoare logic. When you read about seL4 proving an operating system kernel correct, same. When you read that Praxis proved Tokeneer to EAL5 in SPARK Ada, same. The triple is the price of correctness. Pay it or guess.