标题: 1980 东尼·霍尔 [打印本页] 作者: shiyi18 时间: 2022-4-15 22:33 标题: 1980 东尼·霍尔 C. Antony R. Hoare
PHOTOGRAPHS
BIRTH:
in Sri Lanka in 1934
EDUCATION:
Dragon School in Oxford and King's School in Canterbury. His university undergraduate education was also in Oxford and he did post graduate there as well as Moscow State University.
EXPERIENCE:
Royal Navy (1956-57), Elliott Brothers (1960-1968), Queens’s University, Belfast (1968 - 1977); Oxford University (1977); currently Emeritus Professor at Oxford University and a Senior Researcher at Microsoft Research in Cambridge, UK.
HONORS AND AWARDS:
Turing Prize (1980); Harry H. Goode Memorial Award (1981); Fellow of The Royal Society (1982); Kyoto Prize (2000); Knighted by the Queen for services to education and computer science (2000); honorary Doctorates from several universities; Fellow of The Royal Academy of Engineering (2005); Computer History Museum Fellow (2006); Programming Languages Achievement Award (2011); IEEE John von Neumann Medal (2011).
C. ANTONY ("TONY") R. HOARE DL Author Profile link
United Kingdom – 1980
CITATION
For his fundamental contributions to the definition and design of programming languages.
SHORT ANNOTATED
BIBLIOGRAPHY
ACM TURING AWARD
LECTURE
RESEARCH
SUBJECTS
ADDITIONAL
MATERIALS
VIDEO INTERVIEW
“Tony” Hoare, as he is universally known, was named Charles Antony Richard Hoare when born on 11 January 1934 in the city of Colombo in what was Ceylon but is now Sri Lanka. Tony's parents were involved in the business of what was then the British Empire. Tony received secondary education at the Dragon School in Oxford and King's School in Canterbury. His university education was also in Oxford. His degree course, known as “Greats," involved the study of Latin and Greek as well as philosophy. He chose to study modern philosophy, which provided a path to understand logic.
Hoare discusses his upbringing in Ceylon and undergraduare education in the "Greats" at Oxford.
At the time of his graduation in 1956 Tony was called up into the Royal Navy. On completion of the obligatory two years of military service, he returned to Oxford to study Statistics and began computer programming in Mercury Autocode. He then went as a graduate student to Moscow State University to study Machine Translation with Andrey Kolmogorov. Tony states that it was during this time that he saw the problem of sorting (for dictionaries) as important, and here first thought of the novel sorting algorithm that was to become known as Quicksort.
Hoare recalls the creation of his celebrated Quicksort algorithm.
Returning to the UK, Tony joined a small British computer company called Elliott Brothers. One of his major projects was to lead the team that produced the ALGOL 60 compiler for the Elliott 503 computer. This period of practical industrial projects appears to have provided the inspiration for two major themes that were to occupy Tony's academic career. During a course on the programming language ALGOL 60 (given by Edsger Dijkstra, Peter Landin and Peter Naur) Tony saw that the concept of recursion was the key to lucid expression of Quicksort. This contribution alone would have established Tony's reputation, but far more significant was the appreciation of the crucial role of programming languages that he took from this experience.
What at first looks like a failure was another inspiration from Tony's time at Elliott. He candidly reports that it was the inability to deliver an operating system for the Mark II Elliott 503 that caused him to devote much of his later research to understanding and taming concurrency in program execution.
A happy outcome of this period of his life was marriage to the fellow team member Jill Pym, who became his lifetime companion.
The Turing citation emphasizes Tony's contribution to the design of programming languages. When one thinks of the enormous cost to society of constructing programs, one cannot escape the view that the design of the medium in which programs are expressed is of major importance. Unfortunately software is all too often of poor quality, and some of the blame must rest on the languages in which the software is written. Many security holes that let in “malware" such as viruses could be avoided by using better languages. Furthermore, the annual cost of software errors is estimated to run to tens of billions of dollars. Hoare has repeatedly issued warnings about software design, including the clear message that simplicity and elegance are essential if software is to remain within intellectual control. This message is clearly delivered in his Turing Lecture [3].
So many of Tony's contributions relate to programming language design that it is difficult to choose a single paper for the reader to peruse. Perhaps “Hints on programming language design” [2] is a good place to start. Its 1973 publication date is an indication of how long he has been offering good advice—which sadly has all too rarely been heeded.
The design of programming languages is a fascinating task of balancing a desire for mathematical tractability with the need to recognize the engineering concern of efficient compilation. But there is another issue: if there are to be multiple implementations, (or even an effective sharing of understanding between users and compiler writers) it is essential that the meaning of all programs be well-documented. Taking a term from linguists who studied natural languages, computer scientists refer to this task as recording the “semantics” of a programming language.
When Hoare moved from industry to academia in 1968, his first post was as a Full Professor at the Queen's University, Belfast. For some years, he had been dissatisfied with the accepted way of documenting the semantics of programming languages and had sought a style which permits recording those places where a language designer deliberately leaves some features under-determined. He has described how, on unpacking his papers in Belfast, he became excited by Bob Floyd's 1967 paper “Assigning meaning to programs". Floyd had described a way of adding assertions to flowcharts of programs that made it possible to prove that a program satisfies its specification.
Hoare made two bold additional steps, and his “An axiomatic basis for computer programming” [1] is one of the most influential papers on the theory of programming. First he discarded the flowcharts and developed a logical system for reasoning about programs using specifications of statement behavior that have become known as Hoare triples. Secondly, he argued that his “axiomatic" system could be viewed as an abstract way of recording the semantics of programming languages.
Hoare discusses the definition, origin, and purpose of the "Hoare Triple."
The first of these steps has the profound effect of opening up a way of developing provable programs rather than treating their verification as a post hoc concern. Hoare published a number of developments of this idea, and the pursuit of “Hoare semantics" has had a profound effect on the understanding of programming languages and the task of reasoning about programs. There is a fascinating link back to work by Alan Turing in the late 1940s.
Tony Hoare became a professor at Oxford University in 1977 and there returned to his interests in concurrency. Programming languages started by making at first minor and then more significant abstractions from the instruction set of hardware. Each step raises the engineering concern of whether it is possible to translate programs efficiently into machine code. The progress of increasing abstraction has been difficult, but nowhere more so than in the area of concurrency and here Hoare has made further seminal contributions.
It would offer a huge simplification if one could avoid computer programs interacting with one another, but doing so could reduce potential efficiency of some forms of programs by orders of magnitude. More importantly, once programs interact with the physical world they need to react to events that occur at unpredictable points in time. The early ways of synchronizing concurrency in programs was to permit sharing of variables between parts of a program. But unless careful limitations are put on such sharing, it becomes almost impossible to think about all eventualities. Errors in such programs are as elusive as they are damaging. Hoare himself made some of the most important proposals to constrain such interference. He saw, however, that such shared variable concurrency was fatally flawed.
At Oxford, he made another bold intellectual step: in a 1978 paper in the Communications of the ACM (and subsequently in his book Communicating Sequential Processes [4]) he proposed a language (CSP) where the interaction between programs was limited to pre-planned communications. CSP has inspired a wealth of further research, including tools which have encouraged its use in industrial applications. Initially CSP was only a software tool, but it also gave rise to the Transputer machine architecture.
Hoare discusses the origin of his model of "Communicating Sequential Processes" and the central importance of keeping processes from directly accessing the state information of other processes.
Tony retired from Oxford University in 1999, but not from active research. He joined Microsoft's Research Laboratory in Cambridge (UK) and actively pursued several research ideas. His “Unifying Theories" book [6] has attracted a similar following among researchers as his earlier contributions. With his proposal to pursue research “Grand Challenges" [7], he jointly leads the international initiative on “Verified Software" [8].
Tony has been an inspiration to many researchers, and his “family tree" of PhD students can be seen in the book Reflections on the work of C.A.R. Hoare [9], written in honor of Sir Tony's 75th birthday. It provides an in-depth discussion the influence of his work on current research.
Apart from the Turing Prize, Tony Hoare was awarded the Kyoto Prize in 2000, the year he was also Knighted by the Queen for services to education and computer science. He has honorary Doctorates from several universities and is a Fellow of both The Royal Society and The Royal Academy of Engineering.
