Tony Hoare

Tony Hoare (born 1934) is a British computer scientist best known for inventing the Quicksort algorithm and for developing Hoare logic — the axiomatic framework for proving program correctness that transformed formal methods from theoretical possibility to engineering practice. His 1969 paper "An Axiomatic Basis for Computer Programming" introduced the Hoare triple {P} C {Q}, establishing the logical foundations of program verification.

Hoare's influence extends across programming language design: he developed CSP (Communicating Sequential Processes), the formal language for describing concurrent systems that underpins the Occam programming language and influenced Go's goroutines and channels. His advocacy for null reference safety — including his famous 2009 admission that the null reference was his "billion-dollar mistake" — has shaped modern type systems in languages like Rust and Swift.

Hoare received the Turing Award in 1980 for his contributions to the definition and design of programming languages.

Hoare's career demonstrates that the deepest contributions to computer science come not from solving a single problem but from inventing the language in which problems are stated. Quicksort is an algorithm; Hoare logic is a way of thinking. The latter outlives the former.