In the last ten years we have seen major advances in the technology and application of theorem proving, decision procedures, model checking, and constraint satisfaction. We have also seen major advances in the technology and application of program analysis, optimisation, testing tools, assertion checking, test case generation, specification languages, and the theory of programming. Both these advances have been supported by increasing hardware speeds and growing memory sizes. I suggest the time may be ripe to bring together these technologies to meet an old challenge for Computing Science, that of the verifying compiler. If this is successful, one day we will be able to reduce the staggering overall cost of software error, which has also in the last ten years suffered a major increase.

Tony Hoare, the author of Quicksort, led a team in the early 1960s that designed and delivered the first commercial compiler for Algol 60. His 1969 paper "An axiomatic basis for computer programming" started the field of formal correctness of programs, and he has contributed substantially to that field; in fact, one talks about "Hoare Logic." He is known for his development of CSP -- both a language for communicating sequential processes and a theoretical model for concurrent programming -- and has made numerous other contributions to programming, semantics, software engineering.  He was a Professor at Queens University, Belfast, from 1968-1977 and at Oxford thereafter. Since his retirement from academia in 1999, he has worked at the Microsoft Research lab in Cambridge. Among his numerous awards are ACM's Turing Award in 1980 and the Kyoto Prize in Advanced Technology in 2000. He was knighted by Queen Elizabeth in 2000, and that is why some call him "Sir Tony".