There aren't many computer algorithms famous enough to get their very own birthday party, but Quicksort is one of them. Invented by the computer scientist Tony Hoare and published in July 1961, the algorithm's task is to put lists of things into the correct order: numbers in numerical order, words into alphabetical order, or dates into chronological oder. It does this so successfully, it is still hailed as one of the best sorting algorithms and implemented in many programming languages and libraries.
Tony Hoare, the inventor of Quicksort, in 2011. Photo: Rama, CC BY-SA 2.0 FR
Quicksort's anniversary is being celebrated at the Isaac Newton Institute for Mathematical Sciences (INI) in Cambridge this month, and it's from the INI that Hoare (virtually) told us the story of his clever invention and its role in launching his career in computer science. You can read about this story, and the workings of Quicksort, in this article.
Beyond Quicksort
However, inventing Quicksort, Hoare told us, wasn't his only shrewd career move. We all know what it feels like when a computer crashes or software doesn't work: it's frustrating, time consuming, and potentially expensive. If a piece of software controls, say, a plane or a spacecraft, failure could be disastrous. "If you have any application where one error is one too many, you have to have proof [that the program works]," says Hoare.
So back in 1969, inspired by work of the computer scientist Robert W. Floyd, Hoare decided to turn his attention to program proving — not in the sense of chasing through individual programs in search for bugs, but in the sense of creating a general framework that would enable people to both specify their programs correctly and verify them. Hoare was aware of the academic nature of such an undertaking, which would provide him with a lifetime of work.
"I reasoned that this topic was unlikely to find application in industry until the days of my retirement," he says. "Thus there was no risk that my research would be overtaken by the vast sums of money that industrial management can spend on a research project once it is recognised that the project is of value to the company. I am glad to report that, even now, I have never had to change the topic of my research."
Inspiration from maths
An interesting milestone in this work of Hoare's took inspiration from the ancient Greek mathematician Euclid, who created an elegant framework of axioms and rules for geometry. "Euclid designed a language in which he wrote his [geometric] constructions," says Hoare. "At the same time he created a language in which he could specify the theorems he wanted to prove. And it all meshed together perfectly in [a series] of thirteen books. It's fascinating!"
Euclid of Alexandria
Just like geometry, computer programming is an exact science. In principle, you can work out what a computer program is doing just by looking at the code and using some deductive reasoning. Euclid's geometry is built around self-evident truths (axioms) such as "the shortest distance between two points is a straight line" and tells you how to make valid logical inferences. But what should the axioms and rules of inference for computer programming be? Hoare's An axiomatic basis for computer programming, published in 1969, strove to answer these questions and has been hailed one of the most influential papers in the theory of programming. It was just part of a body of work that earned Hoare the prestigious Turing Award in 1980, for "his fundamental contributions to the definition and design of programming languages".
The verified software initiative
Another source of inspiration arrived in 2003 and again came from anther area of science. The human genome project whose aim was to decode the entire human genome, was finally completed after a thirteen year collaborative effort by many scientists.
The verified software initiative takes its inspiration from the human genome project.
"I took that project as a model for deciding what the features of a successful 'grand challenge' project should be," says Hoare. He then issued his own grand challenge for computing research: the construction of a verifying compiler, which uses maths and logic to check the correctness of any other computer program it is given as input.
A few years later, in 2007, Hoare co-launched the Verified software initiative, an "ambitious long-term research project toward the construction of error-free software". The first phase of the project envisioned researchers coming up with a comprehensive theory of programming, tools to automate that theory, and a collection of verified programmes that can replace unverified ones in practice.
"The first phase of the verified software initiative concluded last year," says Hoare. "In moving to the second phase I hope we will plan to discuss with the next generation of researchers, as well as established researchers, a more ambitious and integrated plan of research and development. The final phase will consist of the successive rollout of the technology, eventually to the entire programming profession and those who educate the professions that use [the technology]."
Accelerating progress
Today, at the age of 87, Hoare is looking back on a distinguished career that saw him work in both industry and academia, and appears to have no plans of hanging up his boots. To see Hoare himself talk about this career, and his current interests, watch his talk on the website of the Isaac Newton Institute (INI).
Hoare is currently visiting the INI, not only to celebrate Quicksort's 60th birthday, but also to take part in a two-part workshop on verified software, which brings together the best minds in the field. Facilitating exchanges of ideas on mathematical challenges such as the software verification initiative is the express aim of the INI. "The ideals of the Newton Institute are at the very heart of what research is all about," Hoare says. "The facilities it provides are well-tuned to [making] accelerated progress possible."
And who knows — perhaps this accelerated progress will soon lead us into a beautiful new world where computer crashes and faulty software are things of the past.
About this article
Marianne Freiberger is Editor of Plus. She talked to Tony Hoare in May 2021 when Hoare was taking part in the Verified software: From theory to practice workshop run by the Isaac Newton Institute (INI). This article is based on the interview, as well as Tony Hoare's talk at the INI. See here for other articles based on this interview and talk.
This article is part of our collaboration with the Isaac Newton Institute for Mathematical Sciences (INI), an international research centre and our neighbour here on the University of Cambridge's maths campus. INI attracts leading mathematical scientists from all over the world, and is open to all. Visit www.newton.ac.uk to find out more.
