Tony Hoare

Life and career

In 1960, a twenty-six-year-old British visitor to Moscow State University was given the job of writing a program to translate Russian sentences into English. The dictionary lookup required the words of each sentence to be in alphabetical order, and the sorting method he first thought of was slow. Lying in bed one morning, he worked out a better one: pick an element, partition the rest around it, recurse on both halves. He tried to explain it to his supervisor, who bet him sixpence it could not work. Tony Hoare's Quicksort is now sixty-five years old and is still, with engineering refinements, the sorting algorithm most standard libraries reach for.

Charles Antony Richard Hoare was born in Colombo, Ceylon (now Sri Lanka), in 1934, to British parents, and was educated in England — Dragon School, Canford, then Merton College, Oxford, where he read Greats: classics and philosophy, not mathematics. That training shows in his prose, which is among the most precise and least ornamented in the field. After national service in the Royal Navy, where he learned Russian, he studied statistics at Oxford under a young lecturer named John Leech, and then went to Moscow State University to study machine translation with Kolmogorov's school.

Returning to Britain in 1960 he joined Elliott Brothers, a small computer manufacturer, and led the team that implemented ALGOL 60 — an implementation Dijkstra publicly praised, and which Hoare credits with teaching him what a well-designed language could do. It was also at Elliott that he was involved in a large operating system project that failed badly, an experience he later discussed publicly and unflinchingly as the source of his conviction that a design one cannot reason about is a design that will fail.

In 1968 he became Professor of Computing Science at the Queen's University of Belfast, arriving as the Troubles began, and in 1977 moved to Oxford, where he held a chair for two decades and built the Programming Research Group into a leading center for formal methods. Oxford under Hoare produced the Z notation and a generation of verification researchers, and worked with industry — notably a collaboration with Inmos on the transputer, where CSP directly informed the occam language.

He received the Turing Award in 1980. His lecture, "The Emperor's Old Clothes," is a candid account of his own failures and a statement of the principle he is most quoted for: that there are two ways of constructing a software design, one being to make it so simple that there are obviously no deficiencies, and the other to make it so complicated that there are no obvious deficiencies.

After retiring from Oxford in 2000 he joined Microsoft Research in Cambridge, where he worked into his eighties on the "verifying compiler" grand challenge. He was knighted in 2000. In a 2009 talk he apologized for inventing the null reference in ALGOL W in 1965 — he called it his billion-dollar mistake, put in simply because it was easy to implement, and estimated the cost in crashes and vulnerabilities over the following forty years. It is the rare case of a founder of a field publicly auditing his own worst decision.

Key contributions

**Quicksort (1961).** Choose a pivot, partition the array so that everything less than the pivot precedes it and everything greater follows, recurse on the two parts. Average-case *O*(*n* log *n*) comparisons, worst case *O*(*n*²), and — the reason it wins in practice — it sorts in place with excellent cache locality and a very small constant factor. Hoare also gave **Quickselect**, the same partitioning idea applied to finding the *k*-th smallest element in expected linear time, which is the standard algorithm for medians and order statistics. For a statistically trained audience the interesting feature is that Quicksort's average-case analysis is a genuine probabilistic argument over random pivot choices — an early and clean instance of randomization making a worst-case-bad algorithm reliably good, which is the whole logic of randomized algorithms.

**Hoare logic (1969).** "An Axiomatic Basis for Computer Programming" introduced the **Hoare triple** {*P*} *S* {*Q*}: if precondition *P* holds and statement *S* terminates, postcondition *Q* holds. Hoare then gave axioms and inference rules for the constructs of a structured language — an assignment axiom that works by backward substitution, rules for sequencing and conditionals, and a **loop rule** requiring an invariant that is preserved by the body and, combined with the negated guard, implies the postcondition. The result is that program correctness becomes a matter of deriving a proof by induction over program structure, rather than enumerating test cases. Every modern verification tool that talks about preconditions, postconditions, and loop invariants — from JML and Dafny to the SMT-backed verifiers in current use — is applying Hoare's calculus.

**CSP (1978).** Communicating Sequential Processes models concurrency as independent processes that interact only by synchronous message passing over channels, with no shared state. The 1978 paper and the 1985 book develop an algebra of processes with operators for choice, parallel composition, and hiding, and a semantics in terms of traces, failures, and divergences — which makes it possible to *prove* properties like deadlock freedom and refinement of a specification by an implementation. CSP's practical descendants are wide: occam and the transputer directly, and the channel-based concurrency in Go and in Erlang's message-passing style share its central design commitment that shared mutable state is the enemy.

**Data abstraction and structuring.** Hoare's work on "Proof of Correctness of Data Representations" (1972) introduced the **abstraction function** and **representation invariant**: to prove a concrete data structure correctly implements an abstract type, exhibit a mapping from concrete states to abstract ones and show every operation commutes with it. This is the formal underpinning of information hiding and of the abstract data type, and it is the standard technique for reasoning about any encapsulated module. He also contributed the monitor concept (with Per Brinch Hansen) for structured concurrent access to shared resources.

In battle

Hoare's profile is a specialist's: mean 26.1, median 19, five dominant scores, fifty-two problems at or below 20 — but with the single highest category mean of any figure in this cohort, `systems` at 83.0.

**Prove the program correct** (P048) at 97 is his life's work stated as a scenario. Absence of overflow and division by zero are exactly the partial-correctness and safety assertions Hoare triples were built to discharge: annotate the routine with invariants, prove each statement preserves them, and correctness for all inputs follows by structural induction rather than by testing. Note that Dijkstra scores 96 on the same problem, and the two are genuinely close — Hoare's edge is that the axiomatic framing matches the problem's after-the-fact posing, where Dijkstra would insist on deriving the program instead.

**The wall around the data structure** (P254) at 88 is data abstraction, where the abstraction function and representation invariant are his contribution directly. **The machine that overdosed** (P248) at 86 is Therac-25, a concurrency-caused safety failure of exactly the type CSP was designed to make provable, and one his Turing lecture's ethos speaks to. **Every interesting property is undecidable** (P156) at 82 is Rice's theorem, where he is not the author but is the person who spent a career working productively *inside* the limitation it states — you cannot decide correctness in general, so you supply the proof by hand. **Agreement among the unreliable** (P078) at 80 is Byzantine consensus, where CSP's process algebra and his concurrency work give real traction, though Lamport owns the specific result. **The compiler that beats the coder** (P244) at 78 rewards the man who wrote the ALGOL 60 compiler. **Trust without recomputing** (P164) and **Solve the impossible formula** (P187, SAT solving) at 60 sit at the edge of his reach — proof checking and constraint solving are adjacent to verification but belong to others.

His `computability` mean of 38.1 across sixteen problems and `search` mean of 36.9 across fifteen reflect that formal methods touch a lot of theory without owning it.

The floor is a statistician's revenge. He scores 6 on **The pump on Broad Street** (P209, Snow's cholera epidemiology), 5 on **Twenty thousand tests at once** (P124, multiple testing and FDR), 5 on **When the bell curve won't hold** (P126, nonparametrics), 5 on **A hundred sensors for a city's water** (P274, sensor placement), and 3 on **The coefficient that flips sign** (P143, collinearity and confounding) and **The spam in the inbox** (P144, naive Bayes with Laplace smoothing). His `testing` mean is 5.0, `classification` 6.5, `regression` 7.5.

The instructive thing is that Hoare studied statistics at Oxford before going into computing — and it makes no difference to the profile, because none of it entered his research. His entire method is *deductive*: prove a property holds for all inputs. Statistics is *inductive*: estimate a quantity from a sample and quantify how wrong you might be. Those are not neighboring skills; they are opposite epistemologies, and the game scores them that way. Play Hoare on verification, concurrency, abstraction, and sorting. Against anyone holding a dataset, the man who proved programs correct cannot even state the problem.