Tony Hoare, who has died aged 92, did much to transform computer program development from an arcane craft to an engineering profession. He made fundamental contributions to program verification, algorithm design, language semantics and concurrency theory. Initially expressed as theories, many of his ideas eventually became embedded in sophisticated tools that support large-scale programming practices.

The Quicksort sorting algorithm (1961) is still known and used widely in applications organising data of any kind in a specific order. It is an archetypal example of a divide-and-conquer algorithm.

In 1968 Tony left the computer industry to become professor of computer science at Queen’s University Belfast. The following year he began the work that led eventually to an entire family of logics – these days known as “Hoare logics”. They enable software engineers to verify a program’s formal “correctness” – that it behaves as intended. Tony’s revolutionary formalisation of the key ideas as a concise collection of logical inference rules makes it straightforward for a non-specialist programmer to adopt.

In 1977 he was made professor of computation, and head of the Programming Research Group (PRG) of the computing laboratory at Oxford University. His arrival there kickstarted the transformation of the PRG from a tiny group of two academics to a fully fledged computer science department.

The theoretical work he started there on communicating sequential processes (CSP) revolutionised the description and analysis of concurrent and distributed systems in which interactions take place between components and subsystems that run in parallel. It provides the logical framework for an understanding of systems of any scale. Important applications include the checking of software for problems that arise inadvertently and for vulnerabilities to malign intervention by “hackers”.

Born in Colombo, Ceylon (now Sri Lanka), Tony was the son of British parents, Marjorie (nee Villiers), the daughter of a tea planter, and Henry, a colonial civil servant. He was educated at the Dragon school in Oxford and the King’s school in Canterbury.

At Merton College, Oxford, he gained a double first in classics. His philosophy tutor, John Lucas, had taken degrees in mathematics and classics, and Tony also participated in an informal reading and discussion group focused on topics not covered in the classics curriculum: symbolic logic, probability theory, computation and algorithmics.

On graduating in 1956 he took a short course in Autocode programming on the university’s Ferranti Mercury computer. During his 18 months’ national service in the Royal Navy he studied Russian to a level where he could read Russian scientific and technical papers.

In 1959-60 he went to Moscow State University, where he attended lectures given by Andrey Kolmogorov, famed for the clarity of his exposition, and for his work on probability, statistics, information complexity and intuitionistic logic.

While acting as an interpreter at a Moscow exhibition, Tony met executives from Elliott Brothers, a small British manufacturer, who were selling their computer there. Impressed by his Russian, they offered him employment, and he eventually joined them as a programmer when he returned from Moscow. He used to say (tongue firmly in cheek): “They were embarking on the design of a new and very much faster computer (the Elliott 4100), and they thought they would celebrate by inventing a new language to program it in. As a recent employee, with six months’ experience, I was put to designing the language.”

Fortunately, having seen a report on the algorithmic language Algol 60, he was able to persuade the company to implement that, rather than inventing a language of its own. It proved a very good commercial decision; and there, too, he met and in 1962 married Jill Pym, another programmer on the Algol project.

Tony often wrote eloquently of the lessons he learned from his next project, the Elliott 4100 operating system. Elliotts had attempted to develop a multi-user operating system, but the implementation became too large and unstructured to complete reliably, and the system was eventually scaled back to a more conventional form. The company became part of a major government-brokered consolidation of the British computer industry in the late 1960s. By the time this began Tony was set on becoming an academic.

His two universities, Queen’s Belfast and Oxford, were fortunate to appoint a pioneer with Tony’s tastes, experience and temperament to departments whose tradition of teaching had hitherto been mainly in numerical computing, for he revolutionised each of them intellectually during his tenure, while simultaneously revolutionising computer science.

He was characteristically modest when he spoke about his own role in these transformations: “I just found some really good people, then I let them get on with it.”

In fact his inventiveness and his talent for exposition meant that good people sympathetic to his approach flocked towards him; and he had a remarkable capacity for evoking in his collaborators the sense that they were part of a shared scientific and educational mission. He had an extraordinary ability to see links between fundamental research and practical engineering applications and to recruit and guide collaborators to explore them.

Among the collaborations he catalysed was that with Inmos leading to the design in the early 80s of the Transputer: unusual because it combined processor, memory, and communication hardware in a single chip, and was intended for building scalable parallel systems. It was programmed in Occam, a language with semantics rooted in CSP.

A later long-term collaboration with IBM helped the company regain intellectual control of its large, long-lived, transaction processing system. Each collaboration was recognised with a Queen’s award for technological achievement (1990 and 1992).

Tony’s election to the Royal Society in 1982 on the strength of his contributions to programming theory and practice marked the society’s long-delayed recognition of the intellectual status of programming as a science. Its earlier and long-established computing fellows had both been hardware engineers.

When Tony retired from Oxford in 1999 his move to Microsoft Research in Cambridge was natural. Bill Gates had publicly expressed admiration for him, singling out his contributions to algorithm design and programming methodology as deeply influential.

He took his move to be a return to industry, and spent several happy years collaborating with software engineering groups in the company, and enjoying the resources Microsoft was prepared to devote to building tools that supported the scaling up of verification methods to large software systems.

Traditionally, verification systems tried to put everything into one large logic, which quickly became too complicated to reason about automatically. His idea of “combining theories” was an attempt to make formal verification scalable by building verification systems out of composable independent mathematical theories. The central idea of his book Unifying Theories of Programming (with He Jifeng, 1998) took this further and provides a mathematical framework in which different programming paradigms can be expressed in a single semantic universe.

Knighted in 2000, he received the Turing award (1980) for “fundamental contributions to the definition and design of programming languages”, the Kyoto prize (2000), the IEEE von Neumann Medal (2011), and the Royal Medal of the Royal Society (2023) for “groundbreaking contributions that have revolutionised the computer programming field, providing a robust framework for ensuring software reliability”.

He is survived by Jill, his son Tom, his daughter, Jo, and granddaughters, Jhansi and Maya. Another son, Matthew, died of leukaemia in 1981.

Charles Antony Richard Hoare, computing scientist, born 11 January 1934; died 5 March 2026