Sir Charles Antony Richard Hoare (1934 - 2026), known as Tony Hoare, was a British computer scientist who made foundational contributions to programming languages, algorithms, and the formal verification of software.[1] He is best known for devising the Quicksort sorting algorithm and for Hoare logic, a formal system for reasoning about the correctness of computer programs.
Early life and education
Hoare was born on 11 January 1934 in Colombo, in what was then the British colony of Ceylon (now Sri Lanka).[1] He was educated at the Dragon School in Oxford and The King's School, Canterbury, before reading classics and philosophy at Merton College, University of Oxford. He later spent time at Lomonosov Moscow State University, where he studied machine translation and probability theory.
Quicksort and early career
While in Moscow around 1960, working on a project to translate Russian into English, Hoare devised Quicksort, an efficient divide-and-conquer sorting algorithm that remains one of the most widely used sorting methods in computing.[1] He then joined the British computer manufacturer Elliott Brothers, where he led the development of an ALGOL 60 compiler and worked on operating systems.
Formal verification and Hoare logic
In 1968 Hoare became Professor of Computing Science at the Queen's University of Belfast, and in 1977 he moved to the University of Oxford. His 1969 paper "An Axiomatic Basis for Computer Programming" introduced what became known as Hoare logic, a formal system that uses preconditions and postconditions to prove the correctness of programs.[2] He also developed Communicating Sequential Processes (CSP), an influential formal language for describing the behaviour of concurrent systems.
Later career and the "billion-dollar mistake"
After retiring from Oxford, Hoare joined Microsoft Research in Cambridge in 1999. He is also remembered for introducing the null reference in 1965 while designing the type system for ALGOL W, a decision he later regarded as a costly source of software errors.[1]
Honours and legacy
Hoare received the Turing Award in 1980 for his contributions to programming languages and methodology. He was elected a Fellow of the Royal Society in 1982, awarded the Kyoto Prize in Advanced Technology in 2000, and knighted the same year. Later honours included the IEEE John von Neumann Medal in 2011. He died in Cambridge on 5 March 2026, remembered as one of the founders of the discipline of computer science.[1]
References
- Tony Hoare - Wikipedia
- C. A. R. Hoare, "An Axiomatic Basis for Computer Programming", Communications of the ACM (1969)
- C. Antony R. Hoare - A.M. Turing Award, Association for Computing Machinery
- Tony Hoare, "Null References: The Billion Dollar Mistake" (InfoQ presentation)
- Kyoto Prize laureate: Charles Antony Richard Hoare (2000)
