An Axiomatic Basis for Computer Programming Alive

Published in CACM in October 1969, the paper gave programming a logical system: axioms and inference rules for each construct, reasoning about {P} C {Q} — if precondition P holds, executing C leaves Q true. Hoare acknowledged Turing's 1949 'Checking a Large Routine' as predecessor, itself nearly lost.

The framework became Hoare logic — the foundation of Dijkstra's weakest preconditions, modern verification (Coq, Isabelle, separation logic), and contract-driven designs like Ada/SPARK and Eiffel. Every program proved correct descends from this paper's notation.