Celebrating Tony Hoare’s mark on computer science

Tony Hoare at the LASER summer school, September 2007
(All photographs in this article are by Bertrand Meyer)

Had they included just one of Tony Hoare’s major achievements, many scientific careers would be considered prestigious enough. His had a long list, which I am going to try to summarize, not pretending to get anywhere clause to exhaustiveness, on the sad occasion of his passing away last week at the age of 92. (Note: the text as given here is a first draft. I will polish it in the coming days.)

I will talk about the personality of C.A.R. Hoare, more recently Professor Sir Tony Hoare (the initials stand for Charles Anthony Richard but he was always known as Tony) in the second part of this article. I should already note, however, for anyone not familiar with his texts, that “Hoare contribution” also connotes an unmistakable style. In his Turing lecture [1], he stated explicitly that for him there was no clear delimitation between the research and the writing, and it shows. Here for example is his explanation of the (profound) rule that he introduced for the axiomatics of recursion [2] (the “infinite regress” is the initial impression that a call to a routine within that routine will lead to an endless cycle):

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, but this impression is misleading. He started his career as a programmer and manager in industry, an experience that he recounted in his Turing Award lecture [1]. What academic background he did have was unconventional: he was trained in the classics at Oxford. Some of his work reviewed below is deep in mathematics and logic and one wonders how he learned the material. He did not have a doctorate (other than the many honorary ones he gained later). As a matter of fact, trying to name brilliant British pioneers in computer science (other than Turing) immediately brings up names such as Christopher Strachey, Robin Milner, Peter Landin, and Michael Jackson (requirements engineering visionary, and Hoare’s fellow student at Oxford), none of whom, like Hoare, had a PhD. That is not even a purely British phenomenon, since Bob Floyd, pioneer of algorithms and formal methods, is also in this category. Imagine their attempts at an academic career in today’s rule-obsessed system.

A beautiful algorithm and its beautiful description

Et pour un coup d’essai, ce fut un coup de maître
(“As a novice’s debut, it was a master’s stroke”, after Le Cid, Corneille)

Hoare’s name burst into the computer science scene with the publication of a sorting algorithm used today in millions of programs, aptly named Quicksort [3] [4]. Quick because it can sort an array of n elements– that is to say, reorganize them in order of increasing values – in time proportional in most cases to n log n. That means “almost linear” time (where “linear” means proportional to the size n) since the “log” function grows so slowly. To appreciate the importance of this result, one should note that the need to sort lists arises in many, probably most programs, and that the size n can be very large. The simple ideas with which anyone can come up when faced with the task – for example, sweep through the array, swapping along the way any adjacent elements that are in the wrong order, and repeat the sweep until there is nothing left to swap – are “quadratic”, meaning that they take time proportional to the square of n. The difference between linear (or “almost” linear) and quadratic is enormous for large n, even with powerful computers; it can make the difference between an array that we can sort in the blink of an eye and one we could not sort in any reasonable time.

Quicksort is striking in its simplicity and elegance. It is based on the idea that a straightforward linear-time solution exists for a more limited form of the sorting problem, which Hoare dubbed “partitioning” the array: reorganize it so that smaller values appear first, followed by larger values. If we can do this, we have not sorted the array yet, but we have made a big step, since the two slices of the partition are, each taken globally, at their definitive place in the future sorted array. And they are each smaller than the original! So all we have to do is to repeat the process until we get slices that are of size 1 (or zero) and the array will be sorted.

How do we partition the array? First, to define “smaller” and “larger”, we simply choose a value, known as the “pivot”. Small means lesser than the pivot, large means greater. The partition algorithm, key to Quicksort, works like this: 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 two cursors have crossed, we are done: the array is partitioned. If not, we swap the two out-of-place elements, and we continue the process, both cursors picking up where they stopped. The partitioning time is clearly linear since we examine each element just once (the cursors never go back).

To go from the Partition algorithm 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 Tony Hoare as it was on many people at the time, had made recursion and exciting new toy. Quicksort provided a natural use of recursion: you can implement a Quicksort procedure by calling Partition on the array two index markers a and b (initially 1 and n), which yields the partitioning line i, then calling Quicksort again on each of the two slices. For decades computer science courses have used descriptions of Quicksort not just as an algorithm but also as an example of why recursion is useful. (Leslie Lamport showed more recently that recursion is an accidental rather than essential feature of Quicksort [5].) The full algorithm description in [2] is:

if M < N then begin partition (A, M, N, I, J); quicksort (A, M, J); quicksort (A, I, N) end end

(where A is the array and M, N are its overall bounds).

Other than the ingenuity and practicality of the solution, the elegance of its original description [3] captured everyone’s attention. While it did not contain a proof of correctness, it was structured in such a way that verifications soon followed.

Axiomatic semantics

Quicksort, however brilliant and useful, was just an algorithm. Hoare’s next major contribution was foundational; it started a whole new area of development

Right from the start of computing, it had been clear to many people that the effects of programs could be described mathematically; Turing himself wrote a convincing note on the topic, introducing the term “assertion” [6] [7]. Considerable work proceeded in the 1960s on mathematizing programming; not so much syntax (a problem which was largely covered by Chomsky’s work, originally for human linguistics) but semantics, reflected in particular in a 1964 conference (the book appeared in 1966 [8]), with contributions by, among others, McCarthy and the Vienna school, but the formalisms remained difficult to use in practice. A major advance happened with Floyd’s 1967 paper associating assertions, in Turing’s sense, with positions in the program [9]. In one of his most famous papers [10], Hoare turned Floyd’s ideas into a full-fledged axiomatic theory, giving birth to “axiomatic semantic”, also known nowadays as “Hoare logic” [11] [12].

The idea, based on the principles of mathematical logic, was brilliant: define a programming language as a mathematical theory – along the lines of axiomatic systems introduced by the likes of Russell, Zermelo, Fraenkel, Von Neumann and Bernays in the early 20^th century – to enable proving prove properties of any program in the language, for example

{n > 5} if m < -3 then n := n + m else n := n – 2 end {n > 4}

This formula (subject to proof or disproof in the theory) is a so-called “Hoare Triple”, {P} A {Q}, expressing that an execution of A started in a state satisfying P will yield a state satisfying Q. Here if we start with n greater than 5 we end up with n greater than 4. (And no, there is no typo in the example. The triple is not the strongest we can derive but it holds.) The way this works is that the theory consists of an axiom or inference rule for every construct of the language; for example the axiom for assignment (“:=”) is {P [E / n]} n := E {P}, working backwards, where P [E / n} denotes the assertion P in which every occurrence of n has been replaced by the expression E, textually (a concept that comes from lambda calculus, designed by Church and Curry in the 1930s, and works whether or not E includes occurrences of n, as it does in the above n := n + m example).

The beauty of this approach is that the rules are defined in a completely formal way, meaning that they work mechanically on program texts. You can apply them blindly without to intuition (“the program does this or that”), and you can ask a computer program – a program verifier – to apply them for you. In the following fifty years, right up to now, program-proving systems have been built on the approach introduced by this paper and later theoretical refinements by Hoare himself, Dijkstra and others.

The original paper contained rules for simple programming constructs. Over the following years Hoare extended the theory to more challenging mechanisms: routines and recursion [2] (from which the excerpt at the beginning of this article comes), data structures [13]. The latter paper is remarkable since it contains the first ever occurrence – a single one, without much commenting – of the fundamental notion of class invariant.

Applications to language design

Although for a large part a theoretician, Hoare was always willing to apply his ideas, perhaps in part because of his industry background. He dabbled in language design, helping Niklaus Wirth [14] to design Algol W [15] 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 a continuation and (most importantly) simplification of Algol 60. It was used for a while as the teaching programming language at Stanford and it was my first real programming-language love, from which I learned a lot (and preventing me from ever switching to its own successor, Wirth’s Pascal).

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” [16]. To continue with citations of (rival) French dramatists of the 17^th century, Hoare deserves in my opinion, for this particular design, Ni cet excès d’honneur, ni cette indignité (Racine, Britannicus): neither such excess of honor, nor such indignity. First, the null pointer is essentially inevitable if you want to model the world, which has references (things containing denotations of other things). Second, 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 way in which Hoare rolled up his theoretician’s sleeves to tackle practical problem was his joint work with Niklaus Wirth to provide an axiomatic semantic definition (based, naturally, on the work mentioned above) for the Pascal language [17].

Another case of practical work was his involvement in what was to become the Ada programming language. In the mid-1970s the US Department of Defense launched a tender for the design of a standard programming language. Four teams, color-coded for the sake of establishing a level-playing field, made it to the second round. Hoare and Wirth had consulted for the “Yellow” proposal, which lost to Jean Ichbiah’s “Green” design. One more round remained, involving Green as well as the Red design. I was at that point host to a little twist in the story. I organized a summer school on programming – which turned out to be a memorable event, taking place in July 1978, with three lecturers: Hoare, Barry Boehm (their families became very close on that occasion, for years to come) and Jean-Raymond Abrial. We held a preparation meeting in the preceding Spring, in March I think, with a dinner in an excellent Paris restaurant. Ichbiah badly wanted to enlist Hoare’s help for the final round, managed to invite himself to the dinner, took possession of the seat next to Hoare and the entire evening courted him with an intensity that left no room for the other dinner guests to say anything. The dialog was mostly “I have lost once, I do not want to be associated with a second loss!” versus “this is your opportunity to erase that episode and leave with a success!”. What Ichbiah most wanted from Hoare, I think, was help in designing the concurrency mechanism. Indeed, Ada’s final “rendezvous” concurrency mechanism was largely derived from Hoare’s CSP (discussed below), which had just appeared at the time.

In the end Hoare did not directly participate in the design but was listed as a member of an advisory committee for it. That role, and the use of his CSP ideas, did not deter him from criticizing the design of Ada, rather harshly, in his Turing Award lecture [1].

Programming methodology

In the earlier years – particularly the 1970s – the profession viewed Hoare as a proponent of disciplined programming methodology. People were realizing that software development required engineering principles. The principal proponent of that school was Edsger Dijkstra, accompanied in the public mind by Hoare and Wirth, and also by such important figures as David Gries, David Parnas and Harlan Mills. The impetus came with the publication in 1972 of the book Structured Programming [18], 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, the first ever, to the ideas of object-oriented programming. Hoare was instrumental in rewriting Dahl’s prose into more standard English.

Everyone in the profession read the book at the time of its publication. Most people stopped at the first or second chapter, finding the third a bit abstruse. As a student I was advised to read the book and fell in love with the third chapter, giving me a great chance to discover OOP before most people paid any attention to it. One of the many ways in which I remain indebted to Tony.

Concurrency

Some of the hardest problems of programming arise when we are dealing with several computations occurring in parallel, and need to handle their synchronization and communication. In the seventies (and to a certain extent still today) the issues occupied some of the best minds in the field, including Dijkstra and Lamport. The challenge was to find, for concurrent programming, mechanisms at the same level of clarity, abstraction, understandability and (through axiomatic techniques introduced by Floyd, Hoare and Dijkstra) provability as sequential programming. (Dijkstra, for example, did not enjoy it at all when people remarked in jest that semaphores, his invention for concurrent programming, were at the same low level of abstraction as the object of his contempt in sequential programming, goto instructions.)

A significant innovation was the introduction of a programming language construct, monitors [19]. (Per Brinch Hansen published a paper on monitors at about the same time; I do not know if the matter of precedence has ever been resolved.) A monitor is a module which gathers a set of potentially concurrent operations on a resource. Monitors are only a language construct, however, and lack the formal specification that one needs to reason rigorously on the concurrent programs.

Hoare felt that more abstraction was needed, away from the constructs of programming languages. Hence the first version of Communicating Sequential Processes (CSP), published in 1978 [20]. A key insight at that point was to consider what may be the two core challenges of concurrency, synchronization and communication, and decide which was the most important. If you have different activities (such as processes or threads) going on in parallel, they must occasionally synchronize with each other, for example when they need access to a limited-sharing resource such as a printer or a communication line; and they must occasionally communicate data to each other. The decision in the initial CSP was to consider communication as the primitive operation, based on the observation that for P to send out some data and Q to receive it, they must both be ready for it; in other words, they must synchronize. Communication, then, implies synchronization (but not the other way around). Hence the “C”, for Communicating, in CSP. Processes (the “P”) can use channels for communication. Two basic operations in which a process can engage are output and input, written (for a channel c):

c!x — Output x on channel c

c?x — Wait for an input x to come through channel c

A key CSP ingredient in using these mechanisms is non-determinism, in part a consequence of Dijkstra’s “Discipline of Programming” work [21]. (No doubt historians of science will study the interplay of influences between Hoare and Dijkstra in those years, including Dijkstra’s extension of Hoare logic into the “calculus of weakest preconditions” in the same work [21].) Non-determinism, using Dijktra’s notation P [] Q (perform either P or Q) applies in particular to input: you can write something like

c1?x 🡪 op1 (x) []

c2?x 🡪 op2 (x)

meaning: obtain a value from either channel c1 or channel c2, whichever comes first, and do something (different) with it. Ada’s Rendezvous mechanism implement this idea in the form of a programming construct.

We had the privilege, at the 1978 summer school, of hearing one of the very first presentations of CSP; Hoare had just designed it back then, and devoted his entire set of lectures to it.

I mentioned Hoare’s inimitable style and here is one example from those lectures. His explanation of the above non-deterministic construct ran like this. You are waiting for a bus, he said; how can you wait faster? Obviously, the audience was bemused and said nothing. The answer, he continued, is to wait for more than one bus at the same time. For example, you are at Peartree in Oxford and want to go to the main station, you can use line 300 (Park & Ride) or S2 (Stagecoach). You can choose one of them and wait for its bus, but you can “wait faster” by waiting from the first bus that comes for either of these lines. That is the essence of the CSP non-deterministic-input construct.

Tony Hoare, Marktoberdorff summer school, August 2004

In his subsequent CSP work in the 1980s, Hoare continued the move away from programming languages and made CSP more general (keeping the acronym but ceasing to expand it since it turned about to be about much more than just sequential processes and their communications). CSP became one of a number of “calculi” – the other most famous one being Milner’s CCS, Calculus of Communicating Systems – providing algebraic frameworks to describe general computations. The new CSP was described in a book by Hoare [22] although a more up-to-date and extensive description can be found in Bill Roscoe’s own book [23].

To describe computations, the new CSP uses a small set of primitive operators which serve to combine processes. Among the most important operators are external choice P 🞏 Q (the environment decides to present you with P or Q and you have to deal with whatever comes, pretty much in the tradition of the original CSP’s non-determinism), internal choice P Π Q (you may decide to perform P or Q), parallel operation P ||_E Q (execute P and Q in parallel, synchronizing on some agreed-upon events, the members of E), hiding (enabling you to choose your level of abstraction by ignoring some events) and recursion. Then, in the tradition of Hoare’s 1969 Axiomatic Semantics work, the theory asserts a number of axioms describing the properties of this operator. Throughout his career Hoare was an advocate of the axiomatic method pioneered by Russell, who allegedly (I have not been able to find this citation outside of Hoare’s own citations of it) characterized it as having “all the advantages of theft over honest toil” – one of the places where the biographer has to acknowledge that some of the more extreme pronouncements of British humor will forever remain impenetrable to the rest of humankind.

A leader and catalyst

Mathematicians are like Frenchmen: you give something to them,
they translate it into their own language, and it becomes something entirely different.
Goethe

CSP triggered a veritable flowering of interest in formal methods and concurrency, particular among researchers who at some point went through the legendary Oxford Programming Research Group. Hoare, educated at Merton College in Oxford, went back as a professor in 1977, taking over from the computer science pioneer Christopher Strachey (another fascinating figure, quintessentially English). Hoare had an extraordinary talent for bringing brilliant people and helping them develop their own strengths. In the early eighties, for example, he brought to Oxford the creators of two major formal specification languages: Cliff Jones with VDM [24], Jean-Raymond Abrial with Z [25]. At Oxford, Z actually underwent a systematic rework, reminiscent of the Goethe quip [26] reproduced above, with Frenchmen and mathematicians replaced by English mathematicians/computer scientists. The new version enjoyed immense success in England, won a Queen’s Award and was used not only academically but in many mission-critical applications in industry, leading to a number of startups and work by such researchers (all having gone through Oxford at some point) as Jim Woodcock, Carroll Morgan, Jim Davies, J. Michael Spivey, Ian Hayes and Ib Holm Sørensen [27].

Another example of the consequences of the extraordinary intellectual climate at Oxford at that time is the work by Cliff Jones on rely-guarantee, an extension of Hoare logic to concurrency [28].

Some scientists are great in their own right; some are also great managers, lead scientific schools and leave a profound influence on many people’s careers. Examples of someone leaving both kinds of legacy exist (think David Hilbert) but are not frequent. Hoare was one of them. One token of his role as leader was his editorship of the Prentice Hall “Computer Science Series”, which published dozens of influential titles in theory, programming languages, semantics and programming methodology in the 1980s and 1990s, with the support of a great editor, Helen Martin, who had barely passed the age of twenty when she started. (Many of the Prentice Hall books cited in the bibliography are from that series.) More generally, he corresponded with many people, in particular younger scientists, and guided them through their careers. One of the fun and instructive experiences at the colloquia which were held in his honor, particularly on the occasion of his successive alleged “retirements” [29] [30], was for someone to explain during some conversation that he had a privileged relationship with Tony, and to discover that everyone else in the group thought exactly the same. He took a genuine interest, pursued over many years, in others’ intellectual development. Let me cite a personal example. After I had published some critical comments of supposedly object-oriented languages, he wrote to me (29 August 2002):

I have been much influenced by Peter Medawar and Richard Doll in working out my own emotional attitude to the issues that you discuss. Medawar says that the true scientist always praises the work of his predecessors, and points out all the defects of his own. I justify this by analogy with the film world: on a film set, the level of stress is so great that everybody is very friendly to each other, on first name terms, ‘ darling..’, ‘that was wonderful but..’. It’s the only way to survive the stress, to build up everybody’s self-confidence. Research is an equally demoralising occupation, and needs something of the same conventions.

Although (as I pointed out to him) that advice did not completely fit with his own criticism of Ada in his Turing Award lecture, I took the lesson to heart, including his own advice in the same message of underselling one’s own work and over-acknowledging that of others, which I have often repeated to students (as the natural tendency in a paper presenting your own latest and greatest work is to do exactly the reverse).

As another example of his role as catalyst, I vividly remember visiting him in Oxford circa 1984, and giving a talk where he basically made up the audience, with at most two or three other people (another sign of his availability and willingness to listen to the ideas of others). The background is that I had published a programming treatise and textbook in French in 1978, which I showed to him on the occasion of the summer school, upon which he immediately said that I should publish a translation in his Prentice Hall series. When I asked if he knew a translator he replied that I should do the translation myself, which I accepted, foolishly since the obvious happened: instead of translating I started to produce something completely new, part of which I was presenting on that day in Oxford. To explain what I was doing in logic-driven software architecture I looked for a good metaphor and, on the spot, proposed that there was a kind of “contract” between caller and callee. He did not say anything, but his mere presence had enabled me to make my incipient ideas gell. Many people could cite similar experiences.

As yet another case of Hoare’s outreach beyond his own contributions, he was a key figure in the IFIP (International Federation for Information Processing) Working Group 2.3 on programming methodology. An IFIP WG is a kind of co-opted scientific discussion club. One of the original WGs was 2.1, in charge of developing a successor to the IFIP-originated and enormously influential Algol 58 and Algol 1960 programming languages. WG 2.1 veered into producing a highly powerful language, which became Algol 68. Wirth, supported by Hoare, proposed a much simpler new design, Algol W (which I discussed above). Upon its rejection by the group, a number of dissenters including Wirth, Dijkstra and Hoare created a splinter group, 2.3, devoted to programming methodology, which meets every few months (now 71 meetings since the first one in Oslo in 1969!). Hoare was a stalwart of the group since its beginning, attending its meetings until recently, that is to say, for over a half-century; WG2.3 was another venue in which he exerted influence on and provided advice to several generations of researchers.

Going back to learn

J’ai plus de souvenirs que si j’avais mille ans
Baudelaire, Les Fleurs du Mal
(“I have more memories than if I were a thousand years old”)

Having retired from the University of Oxford in 1999, Hoare moved over right away to Microsoft Research, as a Principal Researcher at the newly created lab in the UK directed by Roger Needham. Surprising many people (since he had always had a reputation as an Oxford man), the move was also to Cambridge, seat of the new venture. Cambridge MSR quickly became one of the most prestigious computer science labs in the world.

That move also coincided with what some perceived as a change of attitude. 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. At the time of his transfer to Microsoft he became more attuned to the constraints of industry and the need to deal with programs as they are, not just with programs as they should be. I remember hearing him quip – verbally – that “Java should be considered one of the laws of nature” (not something I would ever agree with). He was concerned in particular with the weight of legacy code, all that baggage accumulated over decades of more or less careful programming (recalling, to me, Baudelaire’s verse). In the email message to me quoted earlier he wrote:

I should also commend the alternative approach of designing better libraries and better languages. Both you and Niklaus [Wirth] make the same point. That must be the right way in the long run. But before this can have effect, you will need to rewrite a lot of the functionality of legacy code. So you will need to find out what legacy code actually does. My project may help to do this.

and concluded with a formula that struck me: “That is why I take a somewhat intermediate position – ‘supping with the devil’, you may say. Well, perhaps somebody has to do that too”. He had opted for pragmatism.

What struck me most during those years (the early 2000s) was his incessant thirst for learning. That was not something new: year after year, conference after conference, he was always sitting in the first row, with his big black notebook, carefully taking down what the speakers were saying. All the more striking that so many other people, obviously preoccupied with very important affairs, keep hacking at their laptops (later, phones). He had as many responsibilities as anyone else but when he had an opportunity to learn from others he used it.

I saw him at Microsoft Research in Redmond in a small meeting room, listening to a young engineer describing the intricacies of .NET, and asking patient questions to make sure he understood the details. I believe this particular combination, which I have seen in very few people, is one of the marks of a great scientist: a particular combination of pride and humility. Humble does not mean modest. Hoare was conscious of his accomplishments and I would not call him modest, but he was humble in the sense of always standing ready to go back to the school benches and start learning from the ground up.

The Grand Challenge and Unified Theories

Like many influential scientists, Hoare became preoccupied in the later part of his career with issues of a general scope.

On the theoretical side, he was concerned about the wealth of different approaches to describing programming languages, including two seminal contributions: his own, with axiomatic semantics (“Hoare Logic”); and the work originated by Dana Scott and Christopher Strachey on denotational semantics, for which he had considerable respect. The first “talks about” programs, expressing their properties; the second one “defines” programs as fixpoints of functions on specific spaces. Anyone who has looked at both (or their combination in approaches such as the Cousots’ abstract interpretation [31]) has experienced the intuition that there must be a way to integrate them. Such is the goal of Hoare’s work, with He Jifeng, on “Unifying Theories of Programming” [32]. While it has been influential, this work, I think (in the spirit of this note, which is admiring but not hagiographic) that it has not truly succeeded in its unification goal; something more fundamental remain needed to explain programming.

Another major undertaking, in Hoare’s indefatigable role as organizer and catalyst, was his “verifying compiler grand challenge” initiative. In keeping with his foundational work on software correctness, he proposed the idea of a major project devoted to producing a tool that would produce programs guaranteed correct, not just type-wise, as with the compiler for any statically typed language, but in terms of their semantics: the correctness of their results. After a while he removed from the name the term “compiler”, considered too technical for a wide audience (including possible grant givers), leaving simply “The Verified Software Grand Challenge”. A first conference on the topic was organized at ETH Zurich in 2005, under the name VSTTE: “Verified Software: Tools, Theories, Experiments”, with widely circulated proceedings [33]. The conference has had many more sessions since then, with the 18^th edition scheduled to take place in Graz in September 2026.

Tony Hoare at the VSTTE conference, Zurich, October 2005

Hoare’s original idea for the Grand Challenge did not pan out: he envisioned a major government-funded collective effort to solve the verified software issue, modelled after (for example) the Manhattan project or the decoding of the human genome. That did not happen; governments did not respond on that scale. Numerous smaller-scope projects, however, did take place, and Hoare’s prestige as well as his energy in promoting the idea served as a jolt forcing the computer science and software engineering community to devote renewed attention to software verification and to produce in recent years a spate of powerful program-verification tools – most of them, naturally enough, based on ideas that go back to Hoare’s 1969 Axiomatic Semantics paper.

A mark for the ages

I have often remarked how astounding the opportunity has been, for a computer scientist active in the past few decades, to interact with the giants of the field, as if one had met in a single lifetime (thanks to the short and compressed history of the field) with the equivalents of Archimedes, Descartes, Newton, Einstein and Planck. Hoare was one of these giants, active on so many fronts, defining so many seminal concepts.

I have tried to give an idea of the scientist and the leader, and also, in the background, of the man. Let me conclude, rather than words, with two pictures [34]. One (grainy, sorry) is of Tony with his wife Jill, who was such a strong presence in his life. The other is of him at Munich airport, after a Marktoberdorff summer school, I think in August 2004. I had a rented car and had driven him back to the airport, providing the opportunity of a long discussion on whether Dijkstra, in his attitude towards test, was influenced by Popper’s comments about falsifiability. For some reason he had been given two umbrellas and for some other reason he had two hats. They did not fit into his luggage. 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 rain-protected Tony was too good to miss. There is a lot of him in this picture: the humor hiding under the seriousness (or maybe the other way around), the acceptance of things as they are, the willingness to put up with a bit of absurdity. We miss him.

References and notes

1. C. A. R. Hoare: The Emperor’s Old Clothes, in Communications of the ACM, vol. 24, no. 2, pages 75–83, 1981, available at https://dl.acm.org/doi /10.1145/358549.358561.
2. C. A. R. Hoare: Procedures and parameters: An axiomatic approach, in Symposium on Semantics of Algorithmic Languages, edited by E. Engeler, pages 102–116, Springer, 1971, available at https://dl.acm.org/doi/10.5555/63445.C1104361.
3. C.A.R. Hoare: Quicksort, in The Computer Journal, vol. 5, no. 1, pages 10–16, 1962, available at https://www.cs.ox.ac.uk/files/6226/H2006%20-%20Historic%20Quicksort.pdf.
4. C.A.R. Hoare: Algorithm 64: Quicksort, in Communications of the ACM, vol. 4, no. 7, page 321, 1961, available at https://dl.acm.org/doi/10.1145/366622.366644.
5. This version of Quicksort was mentioned by Leslie Lamport in a video lecture but he has not published it. Calling it “Lampsort”, I described it in B. Meyer: Lampsort, blog article in Technology+ blog, 7 December 2014, available at https://bertrandmeyer.com/2014/12/07/lampsort/.
6. Alan Turing: Checking a large routine, Report of a Conference on High Speed Automatic Calculating Machines, 67–69, 1949. Best read as included, corrected and discussed in the following entry [7].
7. F. L. Morris and C. B. Jones: An early program proof by Alan Turing, in Annals of the History of Computing, vol. 6, no. 2, pages 139–143, 1984, available at https://ieeexplore.ieee.org/document/5011915.
8. T. B. Steel (ed.): Formal Language Description Languages for Computer ProgrammingNorth-Holland, 1966.
9. Robert W. Floyd: Assigning Meanings to Programs, in Proc. American Mathematical Society Symposia in Applied Mathematics, vol. 19, pages 19–31, 1967, available at https://link.springer.com/content/pdf/10.1007/978-94-011-1793-7_4.pdf.
10. C. A. R. Hoare: An axiomatic basis for computer programming, in Communications of the ACM, 12(10), pages 576–580, 583, 1969, available at https://dl.acm.org/doi/pdf/10.1145/363235.363259.
11. Krzysztof R. Apt: Ten Years of Hoare’s Logic: A Survey—Part I, ACM Computing Surveys, vol. 13, no. 3, pages 431–483, 1981, available at https://dl.acm.org/doi/10.1145/356850.356855.
12. Krzysztof R. Apt: Ten Years of Hoare’s Logic: A Survey—Part II: Nondeterminism, ACM Transactions on Programming Languages and Systems, vol. 6, no. 1, pages 1–39, 1984, available at https://dl.acm.org/doi/10.1145/357233.357234.
13. C.A.R. Hoare: Proof of Correctness of Data Representations, in Acta Informatica, vol. 1, no. 4, pages 271–281, 1972, available at https://link.springer.com/article/10.1007/BF00289507.
14. The references to Wirth, Boehm and Ichbiah are hyperlinks to obituaries I wrote for each of them.
15. Niklaus Wirth and C. A. R. Hoare: A contribution to the development of ALGOL, in Communications of the ACM, vol. 9, no, 6, pages 413–432, 1966.
16. C. A. R. Hoare: Null References: The Billion Dollar Mistake, QCon London, 2009, abstract available at https://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare/.
17. C. A. R. Hoare and Niklaus Wirth: An axiomatic definition of the programming language Pascal, Acta Informatica, vol. 2, no. 4, pages 335–355, 1973.
18. O.-J. Dahl, E. W. Dijkstra and C. A. R. Hoare: Structured Programming, Academic Press, 1972.
19. C. A. R. Hoare: Monitors: An operating system structuring concept, in Communications of the ACM, vol. 17, no. 10, pages 549–557, 1974, available at https://dl.acm.org/doi/10.1145/355620.361161.
20. C. A. R. Hoare: Communicating sequential processes, in Communications of the ACM, vol. 21, no. 8, pages 666–677, 1978, available at https://dl.acm.org/doi/10.1145/359576.359585.
21. Edsger W. Dijkstra: A Discipline of Programming, Prentice Hall, 1976. This book is a refinement and extension of Dijkstra’s earlier article: Guarded commands, nondeterminacy and formal derivation of programs, in Communications of the ACM, vol. 18, no. 8, pages 453–457, 1975, available at https://dl.acm.org/doi/10.1145/360933.360975.
22. C. A. R. Hoare: Communicating Sequential Processes, Prentice Hall, 1985.
23. A. W. Roscoe: The Theory and Practice of Concurrency, Prentice Hall, 1997, made available by the author at http://www.cs.ox.ac.uk/people/bill.roscoe/publications/68b.pdf.
24. Cliff B. Jones: Software Development: A Rigorous Approach, Prentice Hall, 1980. (To learn about VDM today one should use Jones’s Systematic Software Development using VDM, Prentice Hall, 1990, itself having had a first edition in 1986.)
25. J.-R. Abrial, S. A. Schuman and Bertrand Meyer: A specification language, in On the Construction of Programs, edited by R. M. McKeag and A. M. Macnaghten, pages 343–410, Cambridge University Press, 1980, available at https://se.inf.ethz.ch/~meyer/publications/languages/Z_original.pdf.
26. Goethe’s witticism probably referred to Gérard de Nerval’s translation of Faust into German, which he is said to have preferred, in his old age, to the original.
27. Jim Woodcock and Jim Davies: Using Z: Specification, Refinement, and Proof, Prentice Hall, 1996,
28. Cliff B. Jones: Tentative steps toward a development method for interfering programs, in ACM Transactions on Programming Languages and Systems, vol. 5, no. 4, pages 596–619, 1983, available at https://dl.acm.org/doi/10.1145/69575.69577.
29. A. W. Roscoe (editor): A Classical Mind: Essays in Honour of C. A. R. Hoare, Prentice Hall, 1994.
30. Cliff B. Jones, A. William Roscoe, and Kenneth R. Wood (editors): Reflections on the Work of C. A. R. Hoare, Springer, 2010.
31. Patrick Cousot and Radhia Cousot: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Principles of Programming Languages, pages 238–252, 1977, available at https://dl.acm.org/doi/10.1145/512950.512973.
32. C. A. R. Hoare and He Jifeng: Unifying Theories of Programming, Prentice Hall, 1998.
33. Bertrand Meyer and Jim Woodcock (editors): Verified Software: Theories, Tools, Experiments, First IFIP Working Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions, Lecture Notes in Computer Science, vol. 4171, Springer, 2008.
34. From my “Gallery of Computer Scientists” at https://se.inf.ethz.ch/~meyer/gallery/.