Tony Hoare has died
News of Sir Tony Hoare’s death has prompted reflections on his profound influence on computer science, from inventing Quicksort and developing Hoare logic and Communicating Sequential Processes to pioneering ideas in types, pointers, and formal verification. Commenters recall personal encounters, teaching impact, and quotes such as his “billion dollar mistake” about null references, using them to debate safer type systems, concurrency models, and the unrealized dream of mainstream formal methods. Many emphasize both his technical legacy and his reputation for warmth, humility, and intellectual clarity.
Overall reaction
- Widespread sadness and respect at the death of a foundational computer scientist.
- Many describe him as one of the “greats” whose work underpins large parts of modern computing.
- Several express surprise and disappointment that mainstream media largely ignored his passing.
Key contributions remembered
- Frequently cited: Quicksort; Communicating Sequential Processes (CSP); Hoare logic; monitors; work on ALGOL and structured programming; unifying theories of programming.
- Some argue his most important legacy is Hoare logic and its influence on program reasoning and modern tools (e.g., Dafny, correctness‑by‑construction).
- CSP seen as a core foundation for Occam, the Transputer, Go channels, Erlang-style concurrency, OpenMP ideas, and more.
Null reference and type systems
- The “billion dollar mistake” talk is heavily referenced.
- Consensus: the real problem is making all references implicitly nullable, not the existence of null itself.
- Proposed solutions: optional/maybe types, sum/union types, or explicit “nullable” annotations with non-null as default.
- Debate over ergonomics: some prefer strict typing requiring explicit checks; others want concise syntax but warn against coercing options into booleans.
Formal methods and verification
- Several lament that his dream of mainstream formal verification never fully materialized, despite early successes (e.g., FPU verification).
- Others are cautiously optimistic that code generation plus AI could make proof-assisted development and CbC approaches more practical.
- Linked papers discuss why software became relatively reliable without full proofs and reflect on limits of his original axiomatic program.
Concurrency and system design
- CSP vs. Actor model vs. Software Transactional Memory is debated; some claim actors don’t compose correctness as well as transactional approaches.
- Some worry modern async/await style is discarding the conceptual clarity of process calculi.
- Hoare’s aphorisms about simplicity vs. complexity and the price of reliability are frequently invoked and related to current “move fast” culture.
Personal anecdotes and character
- Many recount lectures and one‑to‑one interactions: he is remembered as humble, sharp into his 80s, generous with students, and unusually kind.
- Stories from Oxford, Cambridge, and various conferences highlight his warmth and gentle humor (including building‑name puns and room dedications).
History and language design debates
- Long subthread on the history of pointers, references, and nulls: multiple early languages and machines are cited; chronology and priority remain contested.
- Discussion of his influence on language keywords (case, class, new), record/structure ideas, optional types, and enumeration types.
- Some note how small, elegant ideas (like Quicksort or CSP) had outsized and enduring impact compared to today’s vast but often forgettable systems.