An Axiomatic Basis for Computer Programming
Prove a program correct, the way you prove a theorem.
What if you could prove a program has no bugs — not test it a thousand times and hope, but prove it, the way you prove a theorem in maths?
The idea, unpacked
Most software is checked by testing: run it on some inputs, see if the answers look right. But testing can only ever show that the cases you tried worked — it can never show that the case you didn't try won't crash. Hoare proposed something stronger: write down, in plain logic, what must be true before a piece of code runs and what will be true after, then prove the link with airtight reasoning that covers every possible input at once.
He wrote it as a little sandwich: a precondition, the program, a postcondition. The trickiest part of any program is a loop, because it can run any number of times. Hoare's key tool for loops is the invariant — one statement that stays true on every single pass, no matter how many times the loop spins. Pin down the right invariant and the loop's correctness falls out.
Where it came from
In 1969, Tony Hoare — already famous for inventing the Quicksort sorting algorithm — was a young professor at Queen's University Belfast. Building on Robert Floyd's 1967 idea of attaching logical assertions to a flowchart, Hoare recast the whole thing in the style of Euclid's geometry: a handful of axioms and rules from which a program's correctness could be deduced.
He was careful about credit, noting that the assertion idea reached back through Floyd to Turing and von Neumann in the 1940s. His own gift was the elegant set of rules — one for assignment, one for chaining steps, one for loops — that made the method clean enough to teach and general enough to last.
Why it mattered
This is the moment programming started to become a science rather than a craft. Hoare's opening line — that a program's behaviour can, in principle, be worked out from its text by pure reasoning — set an ideal the field has chased ever since. For software that absolutely must not fail (aircraft, medical devices, the chip in your car, the kernel of an operating system), 'we tested it a lot' is not good enough; 'we proved it' is the gold standard, and Hoare gave us the language to do it.
A way to picture it
Think of a balance scale you must keep level while you move weights around. A loop invariant is a promise that the scale stays balanced after every single move, even though the weights keep changing. In Hoare's own example — dividing one number by another by repeated subtraction — the promise is 'the part I've taken away plus the part still left always adds back up to the number I started with.' It's true at the start, it's true after every subtraction, and when you can't subtract any more, it tells you the answer.
Where it sits
Hoare's logic is one leg of a great trio about what computers and logic can do. Turing (1936) showed some questions no program can ever answer; Gödel (1931) showed some truths no formal system can ever prove. Against that backdrop, Hoare staked out the bright side: for the programs we actually write, correctness can be proved. His near-contemporary Edsger Dijkstra (whose 1959 shortest-path work is also in this Library) pushed the same banner — 'structured programming' and reasoning about programs as you write them, not after.
In this paper an attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics.
Computer programming is an exact science in that all the properties of a program and all the consequences of executing it in any given environment can, in principle, be found out from the text of the program itself by means of purely deductive reasoning.
If the assertion P is true before initiation of a program Q, then the assertion R will be true on its completion.