GoKawiilTony Hoare at the LASER summer school, September 2007
(All photographs in this article are by the author)
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 close 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 Antony Richard but he was always known as Tony) later in 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” would be the endless cycle that might seem to follow, for someone not mastering recursion, from a call to a routine appearing within the body of that routine):
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 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, 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, any more than Hoare, had a PhD. That is not even a purely British phenomenon, since Bob Floyd, pioneer of algorithms and formal methods, was also in this category in the US, as well as Michel Sintzoff in Belgium. 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)
... continue reading