Presented at a formal methods symposium in 1996, this paper by Tony Hoare addresses an apparent paradox. He had long argued that programs should be proved correct by mathematical means, yet software had become remarkably dependable without such proofs being widely used in industry.

Hoare examines the practical measures that had delivered this reliability: careful management, structured design, thorough testing and debugging, defensive programming, and the cautious, incremental improvement of systems already in use. These methods, he observes, had achieved in practice much of what formal proof aimed at in theory.

Rather than treating this as a challenge to his life’s work, Hoare argues that theory and practice are complementary. Formal reasoning, he suggests, helps to explain why the informal techniques succeed and can guide their further improvement. The paper reflects a considered view of the relationship between mathematical proof and engineering craft.