2008年11月5日，应周巢尘院士邀请，图灵奖获得者C.A.R. Hoare教授访问中科院软件所计算机科学国家重点实验室.

C.A.R. Hoare简介：     C.A.R. Hoare (Tony Hoare)教授，1980年获得美国计算机学会(ACM)设立的计算机界最高奖——图灵奖，2000年获得日本稻盛财团设立的国际大奖 ——京都奖(尖端技术领域)，同年，英国女王伊丽莎白二世授予Tony Hoare爵士爵位，以表彰他对计算机科学所做出的巨大贡献。目前受聘于微软公司。

Hoare教授以图解的方式深入浅出地介绍了他新近关于分离逻辑(Separation Logic)的研究成果。



以上信息来源于中科院软件所

Tony Hoare's interest in computing was awakened in the early fifties, when he studied philosophy (together with Latin and Greek) at Oxford University, under the tutelage of John Lucas. He was fascinated by the power of mathematical logic as an explanation of the apparent certainty of mathematical truth.  During his National Service (1956-1958), he studied Russian in the Royal Navy. Then he took a qualification in statistics (and incidentally) a course in programming given by Leslie Fox). In 1959, as a graduate student at Moscow State University, he studied the machine translation of languages (together with probability theory, in the school of Kolmogorov). To assist in efficient look-up of words in a dictionary, he discovered the well-known sorting algorithm Quicksort.

On return to England in 1960, he worked as a programmer for Elliott Brothers, a small scientific computer manufacturer. He led a team (including his later wife Jill) in the design and delivery of the first commercial compiler for the programming language Algol 60. He attributes the success of the project to the use of Algol itself as the design language for the compiler, although the implementation used decimal machine code. Promoted to the rank of Chief Engineer, he then led a larger team on a disastrous project to implement an operating system. After managing a recovery from the failure, he moved as Chief Scientist to the computing research division, where he worked on the hardware and software architecture for future machines.

These machines were cancelled when the Company merged with its rivals, and in 1968 Tony took a chance to apply for the Professorship of Computing Science at the Queen's University, Belfast. His research goal was to understand why operating systems were so much more difficult than compilers, and to see if advances in programming theory and languages could help with the problems of concurrency. In spite of civil disturbances, he built up a strong teaching and research department, and published a series of papers on the use of assertions to prove correctness of computer programs. He knew that this was long term research, unlikely to achieve industrial application within the span of his academic career.

In 1977 he moved to Oxford University, and undertook to build up the Programming Research Group, founded by Christopher Strachey. With the aid of external funding from government initiatives, industrial collaborations, and charitable donations, Oxford now teaches a range of degree courses in Computer Science, including an external Master's degree for software engineers from industry. The research of his teams at Oxford pursued an ideal that takes provable correctness as the driving force for the accurate specification, design and development of computing systems, both critical and non-critical. Well-known results of the research include the Z specification language, and the CSP concurrent programming model. A recent personal research goal has been the unification of of a diverse range of theories applying to different programming languages, paradigms, and implementation technologies.

Throughout more than thirty years as an academic, Tony has maintained strong contacts with industry, through consultancy, teaching, and collaborative research projects. He took a particular interest in the sustenance of legacy code, where assertions are now playing a vital role, not for his original purpose of program proof, but rather in instrumentation of code for testing purposes. On reaching retirement age at Oxford, he welcomed an opportunity to go back to industry as a senior researcher with Microsoft Research in Cambridge. He hopes to expand the opportunities for industrial application of good academic research, and to encourage academic researchers to continue the pursuit of deep and interesting questions in areas of long-term interest to the software industry and its customers.

以上信息来自微软研究院

托尼·霍尔博士 Tony HOARE  "由国家自然科学基金委员会、微软亚洲研究院和北京大学共同举办的第十届“二十一世纪的计算”大型国际学术研讨会" 演讲者

Presentation Title: A Vision for the Science of Programming

Abstract:
I have a vision of the day when software is the most reliable component of any product or system which it controls. On that day, software developers will be respected as the most reliable of professional engineers. On that day, the science of programming will be recognised as the pure branch of computer science, underlying the practice of software engineering in all areas of application.

The basic topic of study in the science of programming is the computer program itself. Like other basic scientists, we ask the most general and the most fundamental questions about it: ‘What does it do?’ ‘How does it work?’ ‘Why does it work?’ and ‘How do we know that the answers to all these questions are correct?’

Like other basic scientists, we pursue scientific ideals. As the physicist pursues accuracy of measurement; as the chemist pursues purity of materials, so we pursue the correctness of programs, far beyond any immediate or commercially exploitable need.

Our method of research is the standard method of science. We formulate general theories expressed in the language of mathematics, and specialise them to particular applications. We support the theories by accumulation of experimental evidence, drawn from the full range of application. And we use computers extensively, both to conduct and store the results of experiment, and to perform the mathematical calculations and proofs that check conformity between theory and experiment.

When sufficient evidence has accumulated, the theories will be embodied in a suite of Design Automation tools, with coherent coverage of all phases in the lifetime of programs, from requirements analysis through specification, design, coding testing, delivery and subsequent maintenance and evolution. As in other branches of engineering, these tools will automate all necessary deductions and calculations, and will thereby conceal from the professional engineer the unpopular fact that the language of Science, even of Computing Science, is mathematics.

The achievement of my vision will depend on a high degree of co-operation and objectively decided competition between rival and complementary branches of our subject. It will require an increase in the scale and ambition of our research goals which is characteristic of other mature branches of science. It will require the sympathy and support of Computer Scientists from around the world. Perhaps we need to engage ourselves in a Grand Challenge project, similar to those which have led to recent breakthroughs in the basic science of biology.

我个人评注：软件工程与有效的形式化方法相结合会给软件产品与服务带来更好的功能性要求效果，还有更好的非功能性要求效果，这方面的工作任重道远，要做的工作有很多，但是这项工作是相当必要的。

转载本文请联系原作者获取授权，同时请注明本文来自黄富强科学网博客。
链接地址：https://blog.sciencenet.cn/blog-89075-45747.html

上一篇：THE COMPUTER REVOLUTION IN PHILOSOPHY
下一篇：计算科技哲学---伦理学问题研究资料