Knight of the byte rides into sunset

The contributions over four decades of C. A. R. Hoare, now Sir Tony Hoare, to theoretical computer science have been crucial to the early development of high-level computer programming languages, compiler technology, the theoretical underpinnings of the semantics of programming languages, algorithms, principles of concurrency, the transputer and many other areas.

Hoare is probably best known for his Quicksort algorithm, developed while he was working as an interpreter in Moscow, which is still classed as one of the most efficient sorting algorithms. He is also known for the development of Hoare triples, his contributions to axiomatic semantics (Floyd-Hoare logic) that address proof of program correctness, and monitors, used to ensure the integrity of critical components of code in parallel systems. Also noteworthy are his contributions to the theory of concurrency, notably the formal language Communicating Sequential Processes, which allows for the specification, design, analysis and implementation of highly concurrent systems.

In addition, Hoare is famous for his contributions to computer-science education, first in the early 1970s at Queen's University, Belfast, and later at the University of Oxford, where he instigated several degree programmes and led the Programming Research Group to world recognition as one of the premier groups of its kind in research and education.

He has been awarded every major prize in the field, including the Association for Computing Machinery's Alan Turing Award, and the Institute of Electrical and Electronics Engineers' Computer Pioneer Award. He was knighted in the millennium honours list for his contributions to computing and education.

In 1999 Hoare retired from Oxford University and took up a position with Microsoft Research in Cambridge. This book is the proceedings of the symposium held on 13-15 September 1999 at St Catherine's College, Oxford, to mark his retirement.

It is no ordinary proceedings, however. This is a highly polished and extremely valuable collection of papers by some of the top names in the field. A few of those who presented at the symposium do not, unfortunately, have papers in the proceedings. Nevertheless the list of contributors reads like a Who's Who of theoretical computer science, programming-language principles, formal methods and software development.

The broad range of topics covers concurrency and communication, semantics of programming languages, program optimisation, modelling, algorithm analysis, the duration calculus, higher-order logic and much more. As one would expect, Hoare's research interests are also prominent here: abstract data types, concurrency à la CSP, proof and reasoning, non-determinism, language design and algorithms. A few less obvious areas such as graphics and robotics are also covered, but each with a formal (mathematical) emphasis.

Most contributors are Hoare's friends, colleagues and collaborators over the years. The collection contains particularly interesting papers that build on developments of Hoare's: axiomatic semantics (for example,"Probably Hoare? Hoare probably!" by Carroll Morgan, Andrew McIver and Jeff Sanders), CSP (for example, "The successes and failures of behavioural models" by Bill Roscoe, Mike Reed and Robert Forster and "Communicating parallel processes" by Stephen Brookes) and program language design (for example, "Principles of language design and Evolution" by Bertrand Meyer, and "Records, modules, objects, classes, components" by Niklaus Wirth). I particularly enjoyed the contributions of Edsger Dijkstra ("A formula is worth a thousand pictures") and Michael Jackson ("The real world"), which summarise many of their own ideas.

This being an Oxford symposium, the formal languages CSP and Z, for which the Programming Research Group is justifiably famed, are well in evidence.

As usual in proceedings, a few of the contributions are more like extended abstracts than full papers. Unlike most proceedings, however, these are nicely presented and well polished, thanks to the contributors and the editors. The editors have themselves made excellent contributions to the collection.

In many respects, one has to think of this as a book of classic papers rather than a symposium proceedings. The editors have done a very fine job (and one would expect no less from such diligent and experienced researchers as Jim Davies, Bill Roscoe and Jim Woodcock) of combining a large number of contributions from distinguished authors and putting them into a cohesive and indispensable collection that is a fitting tribute to the life, work, and legacy of one of the great researchers and educators in the field of computer science.

Mike Hinchey is director, Software Verification Research Center, University of Queensland, Australia.