Tony Hoare

In The You On AI Field Guide

Hoare and Dijkstra developed their ideas in parallel and in mutual awareness, each sharpening the other's thinking. Hoare's 1969 axiomatic paper gave the logic of correctness a formal basis; Dijkstra's 1975 guarded-commands paper reformulated the logic in terms of predicate transformers that supported program derivation. The two papers together constitute the founding documents of the formal methods tradition.

The partnership extended into the 1972 volume Structured Programming, co-authored by Dijkstra, Hoare, and Ole-Johan Dahl, which consolidated the methodology that had been developing through the 1960s. The volume is the canonical statement of the structured programming position, and the three-author composition reflects the collaborative character of the field at that moment.

Hoare's later work on CSP extended the formal methods tradition into concurrency, an area Dijkstra had also worked on but had not developed as fully. CSP became the foundation for the programming language occam and influenced the design of Go's goroutines and Erlang's actor model. The formal framework remains the standard reference for reasoning about concurrent systems.

Hoare's "billion-dollar mistake" apology for the null reference (2009) is characteristic of his intellectual style and aligns closely with Dijkstra's emphasis on the cumulative cost of small early decisions. The null reference, Hoare noted, was introduced because it was easy to implement; the cost of programmer errors caused by null references over fifty years has been estimated in the billions of dollars. The admission is the kind of honest self-criticism that Dijkstra's framework demands and that the profession rarely produces.

Origin

Hoare was born in 1934 in Colombo, then in Ceylon, and educated at Oxford and at Moscow State University, where he studied under Andrey Kolmogorov. He worked in industry at Elliott Brothers before moving to the Queen's University Belfast and then to Oxford, where he held the Professorship of Computation from 1977 to 1999. He received the Turing Award in 1980.

His subsequent career at Microsoft Research, beginning in 1999, extended formal methods into mainstream software engineering through projects such as the Z3 theorem prover and the Dafny verification language. He remains active as of the mid-2020s.

Key Ideas

Hoare logic as formal machinery. The 1969 paper gave Dijkstra's insistence on provable correctness its technical basis and remains the foundation of program verification.

Quicksort. The 1960 algorithm is one of the most widely implemented sorting routines in computing history, and its correctness proof is a canonical exercise in program reasoning.

The null reference regret. Hoare's public apology for the null reference in 2009 is a model of the honest self-criticism Dijkstra's framework demands.

CSP and concurrency. Communicating Sequential Processes extends formal methods into concurrent computation and remains the canonical reference.

"The Emperor's Old Clothes." Hoare's 1980 Turing lecture is a central document in computing's reflective literature, arguing that the profession's pretense of scientific rigor has often concealed engineering improvisation.