This is Tony Hoare’s inaugural lecture as Professor of Computation, delivered at Oxford University in 1985, nine years after he had been appointed to the role. In it, he argues that programming is at heart a mathematical discipline.

Hoare draws a parallel between writing programs and doing mathematics. Just as mathematicians reason from axioms to prove theorems, he suggests, programmers can use formal methods to reason about programs and to establish that they meet their specifications. On this view, the correctness of a program is something that can be demonstrated by proof, rather than only tested by trial.

The lecture reflects the research that occupied much of his career, including his work on program verification and the logic that bears his name. It makes the case that a firm mathematical foundation offers the surest route to reliable software, and that such theory has practical value for the working programmer.