Tony Hoare and His Imprint on Computer Science

Had they included just one of Tony Hoare’s achievements, many scientific careers would be considered prestigious enough. His had a long list, unfortunately closed by his passing away at the age of 92 on March 5. There is no place to describe them all in detail in the present post. (A longer version appears on my personal blog, which includes a bibliography with over 30 entries.) A good summary of Hoare’s career, by Garfinkel and Spafford, is published on the CACM website.

Beyond the facts of this career, we must note at the outset that “Hoare contribution” also connotes an unmistakable style. In his Turing lecture, he stated that for him there was no clear delimitation between research and writing. Here for example is his explanation of the (profound) rule that he introduced for the axiomatics of recursion:

The solution to the infinite regress is simple and dramatic: to permit the use of the desired conclusion as a hypothesis in the proof of the body itself. Thus we are permitted to prove that the procedure body possesses a property, on the assumption that every recursive call possesses that property, and then to assert categorically that every call, recursive or otherwise, has that property. This assumption of what we want to prove before embarking on the proof explains well the aura of magic which attends a programmer’s first introduction to recursive programming.

Who else writes like this? Style is the defining characteristic of Hoare’s work, not just writing style but scientific style, always elegant and focused on what truly matters.

To many, Hoare appeared as the quintessential computer science professor, and may have cultivated this image (I do not remember ever seeing him without a tie, or have any such photo, and the absence of a suit jacket on the boat above stands out as an exception); but this impression is in part misleading. He started his career as a programmer and manager in industry. The academic background he did have was unconventional: the classics at Oxford. He did not have a doctorate (other than the many honorary ones he gained later).

A Beautiful Algorithm and Its Beautiful Description

Hoare’s name burst into the computer science scene with the publication of a sorting algorithm used today in millions of programs, Quicksort. Quick because it can sort an array of n elements in time proportional in most cases to n log n, meaning “almost linear.”

Quicksort is based on the idea that a straightforward linear-time solution exists for a more limited problem, “partitioning”: reorganize the array so that smaller values appear first, followed by larger values. If we can do this, we have made a big step, since the two slices of the partition are, taken globally, at their definitive places in the future sorted array. And each has fewer elements than the original! It then suffices to repeat the process until we get slices of size 1 (or zero) and the array will be sorted.

How do we partition it? First, to define “smaller” and “larger,” we choose a value, the “pivot.” We start from the left of the array (where we eventually want only small elements) and move a cursor right, stopping when we find a large element. Symmetrically, we start another cursor from the right and move left, until we find a small element. If the cursors have crossed, we are done: the array is partitioned. If not, we swap the two out-of-place elements, and continue the process, both cursors picking up where they stopped. The time is linear since we examine each element just once (the cursors never go back).

To go from partition to a sorting algorithm it suffices, as noted, to apply it again to the slices. Quicksort came out at a time when Algol 60, whose influence was fundamental on Hoare as it was on many people at the time, had made recursion and exciting new tool. You can implement a Quicksort procedure by calling Partition then calling Quicksort recursively on each of the two resulting slices. For decades computer science courses have used Quicksort as an example of why recursion is useful. (Leslie Lamport noted more recently that recursion is an accidental rather than essential feature of Quicksort.)

Axiomatic Semantics

Right from the start of computing, it had been clear to many people that the effects of programs could be described mathematically. Hoare turned Floyd’s 1967 ideas into a full-fledged theory, giving birth to “axiomatic semantics,” also known nowadays as “Hoare logic.” The idea, based on the principles of mathematical logic, was brilliant: define a programming language as a mathematical theory to enable proving properties of any program in the language. The rules are defined in a completely formal way, meaning that they work mechanically on program texts. You can apply them blindly, or ask a computer program to apply them for you. In the following 50 years, program-proving systems have been built on the approach introduced by this paper and later refinements.

The original paper contained rules for simple programming constructs. Over the following years Hoare extended the theory to more challenging mechanisms: routines and recursion and data structures (introducing the notion of class invariant). He also applied them to a specification of Pascal, written with Niklaus Wirth.

Applications to Language Design

Hoare helped Wirth design Algol W, a proposed successor to Algol 60 (rejected by the IFIP committee) by bringing in the notion of record (“structure” in C), a programming language invention of which he was proud since it brought to the data side the same kind of structuring mechanism that had been so successful, on the control side, with the control structures of “structured programming.” Algol W was used for a while as the teaching programming language at Stanford and was my first real programming-language love.

Algol W included, along with records, references (pointers), including the possibility of a null pointer. Years later, Hoare stated that it was his “billion-dollar mistake.” Hoare deserves in my opinion, for this particular design, *“*neither such excess of honor, nor such indignity” (using Racine’s famous words in Britannicus), since the null pointer goes at least as far back as NIL in McCarthy’s Lisp (1959), so the mistake, if any, would be shared.

Another case of practical work was his involvement in what was to become the Ada programming language. In the mid-1970s the U.S. Department of Defense launched a tender for the design of a standard programming language. Hoare was involved with one of the losing teams but then became an advisor to Jean Ichbiah’s final design, which incorporated a version of his CSP concurrency mechanism (see below) in the form of the “Ada rendezvous.” That role, and the use of his CSP ideas, did not deter him from criticizing the design of Ada in his Turing Award lecture.

Programming Methodology

Hoare was known, in the 1970s, as a proponent of disciplined programming methodology. People were realizing that software development required engineering principles. The impetus came with the publication of the book Structured Programming (Academic Press, 1972), consisting of three monographs; the first, on structured programming by Dijkstra, expanded on some of his earlier contributions and covered control structures; the second was by Hoare on data structuring. The third, by Hoare again and the Norwegian computer scientist Ole-Johan Dahl, co-creator of Simula 67, had a strange title but was really an introduction to the ideas of object-oriented programming.

Concurrency

A major challenge in the 1970s was to find, for concurrent programming, mechanisms at the same level of clarity, abstraction, understandability, and provability as sequential programming. (Low-level constructs like the semaphore were the concurrent equivalent of the goto, although Dijkstra did not like the analogy.) A significant innovation was the introduction (by Hoare and Brinch Hansen) of a programming language construct, monitors. Hoare felt, however, that more abstraction was needed, away from the constructs of programming languages. Hence the first (1978) version of Communicating Sequential Processes, CSP. The idea was to consider communication as the primitive concurrent operation, since it implies synchronization (but not the other way around). As an example of CSP construct, relying on Dijkstra “[]” non-deterministic operators, you can write something like

c1?x → op1 (x) [] c2?x → op2 (x)

meaning: obtain a value x from either channel c1 or channel c2, whichever comes first, and do something (different) with it. Ada’s rendezvous is based on this idea. Here is how I heard Hoare, with his inimitable style mentioned above, present the topic back in 1978. When you are waiting for a bus, he asked, how can you wait faster? The answer, he continued, is to wait for more than one bus at the same time, assuming that more than one line goes to your destination. You wait faster by waiting for the one that shows up first.

CSP became more abstract in the following years: a full-fledged calculus using a small set of primitive operators such as external choice, internal choice, and parallelism, governed by algebraic laws enabling proofs of the properties of complex computing processes.

Leader and Catalyst

CSP triggered a veritable flowering of interest in formal methods and concurrency, particular among researchers who at some point went through Hoare’s legendary Oxford Programming Research Group. He had an extraordinary talent for bringing in brilliant people and helping them develop their own strengths. In the early ’80s, for example, he brought to Oxford the creators of two major formal specification language, VDM and Z. At Oxford, Z underwent a profound rework, won a Queen’s Award, and was used not only academically but in mission-critical applications in industry.

He corresponded with many people, in particular younger scientists, and guided them through their careers. An important facet of his role as leader was his editorship of the Prentice-Hall “Computer Science Series,” which published dozens of influential titles.

He was a key figure in the IFIP Working Group 2.3 on programming methodology, attending its meetings over a half-century, another opportunity to exert influence on several generations of researchers.

Going Back to Learn

Having retired from the University of Oxford in 1999, Hoare moved over to the newly created Cambridge (U.K.) Microsoft Research lab, which quickly became one of the most prestigious computer science research venues in the world.

Hoare had been associated, together with Dijkstra, Wirth and others, with the programming methodology movement of the 1970s, rightly or wrongly connoting for many people the idea of a disciplinarian attitude towards programming. Having moved to Microsoft, he became more attuned to the constraints of industry and the need to deal with programs as they are, not just as they should be; he was concerned with the weight of legacy code accumulated over decades of more or less careful programming.

What impressed me most during those years was his incessant thirst for learning. In conferences he was always sitting in the first row, carefully taking down what the speakers were saying, even on very specialized or application-oriented topics. I believe this particular combination, which I have seen in few people, is one of the marks of a great scientist: a combination of pride and humility. Humble does not mean modest: Hoare was conscious of his accomplishments and prestige; but he was humble in the sense of always standing ready to go back to the school benches and start learning a new topic.

The Grand Challenge and Unified Theories

Like many senior scientists, Hoare became preoccupied in the later part of his career with issues of a general scope. With He Jifeng, he worked on “Unifying Theories of Programming,” reconciling competing semantic techniques (denotational, axiomatic, operational) in a single framework.

Another undertaking was his “Verified Software Grand Challenge,” a proposal (resulting in the VSTTE conference series) for a major project devoted to producing a tool that would produce programs guaranteed to be correct. It did not succeed in the originally envisioned form of a government-funded collective effort, but was the starting point for the developments that led to today’s powerful program-verification tools.

A Mark for the Ages

Let me conclude, rather than words, with a picture taken at Munich Airport after a meeting in 2004. For some reason he had been gifted two umbrellas and for some other reason he had two hats. I know that does not seem to make sense but somehow the agent had told him he could take everything with him. The opportunity of a picture of a double-hatted and doubly-umbrelled Tony was too good to miss. There is a lot of him in this snapshot: the humor hiding under the seriousness (or maybe the other way around), the acceptance of things as they are, the practicality and earthiness (why renounce any of your possessions?), the mix of apparent shyness and definite self-assurance, the willingness to put up with a bit of absurdity. We miss him.

**Bertrand Meyer **is chief technology officer of Eiffel Software and Recognyze AI (Goleta, CA). He is a Professor Emeritus and former department head at ETH Zurich.

Join the Discussion (0)

Become a Member or Sign In to Post a Comment