Tony Hoare
Microsoft Corporation
|
Primary Section: 34, Computer and Information Sciences Membership Type:
International Member
(elected 2017)
|
Biosketch
Tony Hoare is a Computer Scientist, most famed for his invention in 1960 of Quicksort. His primary degree was in Philosophy, accompanied by Latin and Greek Languages, Literature and History. He holds a professional qualification as an interpreter from Russian to English, and as a Statistician. His main philosophical interests were in mathematical philosophy and epistemology; and he felt that the study of computers could be a source of illumination of age-old philosophical problems of human knowledge and intelligence. His first employment (1960) was as a programmer in the Computer Industry, where he designed an implementation for an innovative programming language ALGOL 60. On moving to academic life in 1968, he proposed a logic for mathematical verification of correctness of computer programs. His theory of concurrency in programming was reported in a well-known article on Communicating Sequential Processes (CSP). It was the basis for the architecture of the INMOS transputer, the first mass-market single-chip networked computer. His subsequent research, in collaboration with He Jifeng, concentrated on Unifying Theories of Programming. On retirement from academic life in 1999, he joined Microsoft Research in Cambridge (UK). His current approach to a Unified Theory is based on a merger of elementary ideas from Geometry, Algebra and Logic.
Research Interests
Tony Hoare’s life-long interest has been in theories applicable to concurrent object-oriented programs. His goal is a theory which aids in the specification, design, development, testing and evolution of comprehensible, correct and efficient computer programs and systems. Recent progress in the research has led to presentations of the same theory in four styles: Geometric, Algebraic, Logical and Operational. (1)Geometry provides the format for diagrams by which the execution of a concurrent program test can be displayed to the programmer. Navigation of the diagram should assist in the interactive detection, location, diagnosis and correction of programming errors. (2)Algebra provides equations justifying optimisations made by the compiler of a programming language, or by the hardware of an instruction pipeline. (3)Logic (in the form of Hoare triples) provides a language for specifying a program, and the interfaces between its parts. Its rules of deduction are intended to assure structural integrity of large program, and correctness of its critical parts. (4)The same logical rules are reinterpreted in the form of Milner transitions to specify operationally the individual step changes in the state of the executing machine. Further work on the theory is required to ensure that the four presentations are consistent when applied to commodity programming languages like C++.
