1980 东尼·霍尔

shiyi18

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.

Author: Cliff Jones



C. Antony R. Hoare

照片
出生地。
1934年在斯里兰卡

教育。
牛津大学的龙门学校和坎特伯雷的国王学校。他的大学本科教育也是在牛津，并在那里和莫斯科国立大学读了研究生。

经历
皇家海军（1956-57），埃利奥特兄弟（1960-1968），贝尔法斯特皇后大学（1968-1977）；牛津大学（1977）；目前是牛津大学的名誉教授和英国剑桥微软研究院的高级研究员。

获得的荣誉和奖项。
图灵奖（1980年）；哈里-H-古德纪念奖（1981年）；英国皇家学会会员（1982年）；京都奖（2000年）；因对教育和计算机科学的贡献被女王授予骑士勋章（2000年）；多所大学的荣誉博士；皇家工程院院士（2005年）；计算机历史博物馆研究员（2006年）；编程语言成就奖（2011年）；IEEE约翰-冯-诺依曼奖章（2011年）。



C. ANTONY ("TONY") R. HOARE DL作者简介链接
联合王国 - 1980年
嘉奖
由于他对编程语言的定义和设计的基本贡献。

简短注释
书目
亚马逊图灵奖
讲座
研究
主题
额外的
材料
视频采访
众所周知，"托尼"--胡尔，1934年1月11日出生在锡兰但现在是斯里兰卡的科伦坡市，名叫查尔斯-安东尼-理查德-胡尔。托尼的父母参与了当时大英帝国的商业活动。托尼在牛津的龙门学校和坎特伯雷的国王学校接受中学教育。他的大学教育也是在牛津。他的学位课程被称为 "Greats"，包括学习拉丁文和希腊文以及哲学。他选择了学习现代哲学，这为他提供了一条理解逻辑的道路。

胡尔讨论了他在锡兰的成长和在牛津的 "Greats "的本科教育。       
1956年毕业时，托尼被召入皇家海军。在完成了两年的义务兵役后，他回到牛津大学学习统计学，并开始用Mercury Autocode进行计算机编程。然后，他作为研究生前往莫斯科国立大学，跟随安德烈-科尔莫戈罗夫学习机器翻译。托尼说，正是在这段时间里，他看到了（字典）排序问题的重要性，并在这里第一次想到了后来被称为Quicksort的新颖排序算法。

Hoare回忆了他著名的Quicksort算法的创造过程。       
回到英国后，托尼加入了一家名为Elliott Brothers的英国小型计算机公司。他的主要项目之一是领导团队为Elliott 503计算机制作ALGOL 60编译器。这段时间的实际工业项目似乎为占据托尼学术生涯的两个主要主题提供了灵感。在一个关于ALGOL 60编程语言的课程中（由Edsger Dijkstra、Peter Landin和Peter Naur讲授），托尼看到递归的概念是清晰地表达Quicksort的关键。仅仅是这一贡献就可以建立起Tony的声誉，但更重要的是他从这一经历中体会到了编程语言的关键作用。

乍看起来是一个失败，但却是托尼在埃利奥特的另一个灵感。他坦率地说，正是由于无法为Mark II Elliott 503提供一个操作系统，导致他后来将大部分的研究投入到理解和驯服程序执行中的并发性。

他在这一时期的一个幸福结果是与同组成员吉尔-皮姆结婚，后者成为他的终身伴侣。

图灵引文强调了托尼对编程语言设计的贡献。当人们想到构建程序给社会带来的巨大成本时，就不能不认为表达程序的媒介的设计是非常重要的。不幸的是，软件的质量往往很差，其中一些责任必须由编写软件的语言来承担。许多让病毒等 "恶意软件 "进入的安全漏洞都可以通过使用更好的语言来避免。此外，软件错误的年度成本估计高达几百亿美元。Hoare多次对软件设计发出警告，包括明确指出，如果软件要保持在智力控制范围内，简单和优雅是必不可少的。这个信息在他的图灵讲座[3]中得到了明确的传达。

Tony的许多贡献都与编程语言设计有关，因此很难选择一篇论文供读者阅读。也许 "关于编程语言设计的提示"[2]是一个好的开始。它的出版日期是1973年，这表明他已经提供了多长时间的好建议--可悲的是，这些建议很少被注意到。

编程语言的设计是一项引人入胜的任务，它要在对数学可操作性的渴望和对高效编译的工程关注之间取得平衡。但还有另一个问题：如果要有多种实现方式，（甚至在用户和编译器编写者之间有效地分享理解），所有程序的意义都必须被很好地记录下来。计算机科学家从研究自然语言的语言学家那里获得了一个术语，将这项任务称为记录编程语言的 "语义"。

1968年，当Hoare从工业界转入学术界时，他的第一个职位是贝尔法斯特女王大学的正式教授。多年来，他一直对记录编程语言语义的公认方式感到不满，并寻求一种风格，允许记录那些语言设计者故意不确定某些特征的地方。他描述了在贝尔法斯特拆开他的论文时，他被Bob Floyd在1967年发表的论文 "为程序分配意义 "所吸引。Floyd描述了一种将断言添加到程序流程图中的方法，这使得证明一个程序满足其规范成为可能。

Hoare做了两个大胆的附加步骤，他的 "计算机编程的公理基础"[1]是编程理论中最有影响力的论文之一。首先，他抛弃了流程图，开发了一个逻辑系统，使用被称为Hoare三元组的语句行为规范对程序进行推理。其次，他认为他的 "公理 "系统可以被看作是记录编程语言语义的一种抽象方式。

Hoare讨论了 "Hoare三要素 "的定义、起源和目的。       
其中第一个步骤具有深远的影响，它开辟了一种开发可证明程序的方式，而不是把它们的验证作为一种事后的关注。Hoare发表了这个想法的一些发展，对 "Hoare语义学 "的追求对理解编程语言和推理程序的任务产生了深远的影响。这与阿兰-图灵在20世纪40年代末的工作有一个迷人的联系。

1977年，Tony Hoare成为牛津大学的教授，并在那里回到了他对并发性的兴趣。编程语言一开始是对硬件的指令集进行微小的抽象，然后是更重要的抽象。每一步都提出了工程上的问题，即是否有可能将程序有效地翻译成机器代码。增加抽象的进展一直很困难，但最困难的莫过于在并发领域，在这里Hoare做出了进一步的开创性贡献。

如果能够避免计算机程序之间的相互作用，这将提供一个巨大的简化，但这样做会使某些形式的程序的潜在效率降低几个数量级。更重要的是，一旦程序与物理世界互动，它们就需要对发生在不可预测的时间点上的事件做出反应。在程序中同步化的早期方法是允许在程序的各个部分之间共享变量。但是，除非对这种共享进行仔细的限制，否则几乎不可能考虑到所有的可能情况。这类程序中的错误是难以捉摸的，因为它们具有破坏性。Hoare本人提出了一些最重要的建议来限制这种干扰。然而，他看到，这种共享变量的并发是有致命缺陷的。

在牛津大学，他在智力上又迈出了大胆的一步：在1978年《ACM通讯》的一篇论文中（随后在他的《沟通顺序过程》一书中[4]），他提出了一种语言（CSP），其中程序之间的互动被限制为预先计划的沟通。CSP激发了大量的进一步研究，包括鼓励其在工业应用中使用的工具。最初CSP只是一个软件工具，但它也产生了Transputer机器架构。

Hoare讨论了他的 "通信顺序进程 "模型的起源，以及使进程不直接访问其他进程的状态信息的核心重要性。       
托尼于1999年从牛津大学退休，但没有从积极的研究中退出。他加入了微软在剑桥（英国）的研究实验室，并积极追求几个研究想法。他的 "统一理论 "一书[6]在研究人员中吸引了与他早期贡献类似的追随者。随着他提出追求研究 "大挑战"[7]，他共同领导了 "验证软件"[8]的国际倡议。

托尼一直是许多研究人员的灵感来源，在为纪念托尼爵士75岁生日而写的《对C.A.R. Hoare工作的反思》一书中，可以看到他的博士生 "家谱"[9]。该书深入讨论了他的工作对当前研究的影响。

除了图灵奖之外，Tony Hoare还在2000年被授予京都奖，这一年他还因对教育和计算机科学的贡献而被女王授予骑士勋章。他拥有多所大学的荣誉博士学位，是英国皇家学会和皇家工程院的院士。

作者。克里夫-琼斯