10月17日，图灵奖获得者、微软剑桥研究院首席研究员托尼·霍尔(Tony Hoare)爵士，与中国科学院院士何积丰、李未、周巢尘、林惠民齐聚微软亚洲研究院，在为期4天的可验证计算大师班里，给中国学生传道授业。托尼·霍尔可谓是可验证软件理论的泰斗，让我们通过下面的对话来了解这位计算大师脑中的奇妙灵感从何而来。 

托尼·霍尔与多位大师坐在讲台上回答学生的问题

问题一：您这次是专门来给“大师班”的学生上课的，可验证软件在中国还是一个全新的课题。能简单地介绍一下您个人在这个领域的发展历史么？

托尼·霍尔：我在这个行业里最早开始自己的工作是在一个比较小规模的英国设备公司，叫做Elliott Brothers。当时主要是为公司提供一种高级语言Algol 60的早期编译器。然后，在1966年的时候，我开始转向从事研究方面的工作。在1968年，我搬到贝尔法斯特开始在皇后大学从事研究和教学的工作。

因为我本人对于编程语言和程序验证以及编程的原则等非常感兴趣，而且当时我们在验证方面也是用计算机本身来做相关的验证和测试，所以，我就开始在皇后大学启动我的研究工作，之后，我写了一系列的论文，主要是以一种相对比较简单的编程语言来从事程序的验证。其实，我当时写这些论文的时候，从来没有预见到，我的这些研究工作在整个行业当中，特别是在接下来30年的时间里能够一直为人们津津乐道。

1999年，我从之前的大学退休。那时候，微软剑桥研究院给了我一个高级研究员的职务。我欣然接受了，而且在这个岗位上一干就是十年。当我进入到微软研究院的时候，我发现我的预测是正确的，正是因为在微软的十年，使得我在过去30年当中的研究想法和成果能有机会转化进产品，在软件的开发方面得到了很广泛的应用。所以，我想在这个领域当中仍然有大量后续的研究需要进行以面对现在计算机行业的新问题。目前来说，计算机要处理的任务的复杂性和规模之巨是从前的人没有预料到的。从这个角度而言，当前的计算机使用规模和复杂性要比30年前大得多。所以，我本人也极力地鼓励我在学术界的同事，以及在大学研究的同行们，能够积极地参与到软件验证的相关研究方面的工作中，使得这样一个非常前沿的研究能够被进一步推进。

非常幸运的是，微软公司有一项政策，那就是积极地参与学术界很有价值的并且和微软有关联的研究工作。我本人也感觉到在推动这方面研究的工作方面，我还是可以为微软做一些贡献，我还是可以在实施微软与大学合作的这个策略和政策方面做一些贡献的。所以，我也积极地和学术界的同事们共同来探讨相关的主题和计划。我们一起发动了一个在研究方面的运动，我们称之为“可验证软件”的倡议。

问题二：听说您当初到牛津大学的时候，学的是文学和哲学这方面的专业，这些可能跟计算机差得有点远，那是什么契机让您转向了学计算机？或者是什么使您对计算机发生了兴趣？

托尼·霍尔：其实是这样的，在那么早期的时候，没有大学专门开设计算机科学的课程，因此，凡是现在从事这个行业的人，早年的时候都是学的别的学科。实际上，当时在大学里，令我最感兴趣的课程是哲学，我当时学两方面的哲学，一方面是古希腊哲学家，比如说像亚里士多德和柏拉图这样的古典哲学；同时，我也学习一些当代哲学家的哲学思想，比如罗素(Russell)和艾耶尔（Ayer）。而在哲学方面令我最感兴趣的课程是数学哲学和科学哲学。即便在当年那样早的时候，哲学家已经对计算这个话题表示出了浓厚的兴趣。在他们看来，计算本身是一种可以用来探索世界、探索人类思维和人类逻辑思考的一个有效途径。

所以说，如果我们的目标是一种模仿人类的智能的方式来对计算机进行编程的话，那首先就必须要对人类的思维、人类的知识、人类的日常生活有所了解。所以，当我发现在这个业界当中有一份等着我去做的程序员的工作时，我就马上来这个公司(微软)了。

我觉得早期学习哲学的经历给予了我在思维的时候一个分析框架的能力，早年的哲学学习给了我一种兴趣和一种能力。也就是说，当我思考一个问题的时候，不管这个问题是什么，我基本上能够从这个问题的所有方面都能够考虑得到，都能够进行思考，接着想出多种不同解决方法。然后，我会选择一个最令人信服的、最好的，甚至是最美的一种解决方法。

问题三：那我想知道一下，您当时在发明快排算法的时候，您当时受到了什么启发或者灵感的来源是什么？您能不能给我们讲一下当时的故事呢？

托尼·霍尔：你问是什么激发了我，其实背后有一个有趣的故事，这个故事说起来非常长。当年我们英国的国家物理实验室给了我一个工作的机会，那个项目主要是做机器翻译语言的方法，把俄语翻译成英语。早在60年代，人们已经开始梦想通过机器自动实现语言的翻译。当时的字典是录在磁带上，所以要找一个词理论上要倒半个磁带，才能找到这个词。那这样的话，在磁头上要花几分钟的时间才可以找到那个词。

那怎么解决这个问题呢？为了克服时间的问题，我们把一个句子当中所有的词，尽量一次性的都查出来。这些词我们按照它在字典当中的顺序来加以排列，然后再到这个磁带当中去找，而不是按照这些词在句子当中的顺序到磁带中间去找。我在1959年时候开始学习编程，我认为如果能够写一个这样的排序的程序的话，应该是一个非常有意思的事情。我当时想到的第一个方法叫做冒泡排序，也就是说一次查一个词。但是，后来我认为这样做的话，查起来就很慢。于是，我接下来的第二个想法就是快速排序方法。

我当时用的理论是一个比较知名而且常用的理论，叫做分治法（Divide and Conquer）。简单来说，在我们解决一个问题的时候，先把这个问题分割成两个部分，那这两个部分呢，比起初的问题要小，但是和原先的问题是很类似的，然后，针对分割出来的小部分别的来找解决方法，然后，再把这两个分别的解决的方法结合起来，回头来解决这个最初的问题，所以，它的英文叫做（Divide and Conquer）。

问题四：听说你在获得图灵奖的时候做了一个名为《皇帝的旧装》的演讲，能说说当时您都谈到了什么？

托尼·霍尔：我在那天的演讲当中主要是谈编程语言的设计，我当时是想对那个时候的一些方法提出一些批评，比如说像Algol 68这样的设计，我认为它们太过复杂了。我就打了一个比方，说这些语言这么复杂，就好像一个人穿了太多件衣服在身上。我就借鉴了安徒生的《皇帝的新衣》的童话故事来说，目前在这样一种情况下，就好像一个人穿了太多件衣服，而皇帝之所以穿了太多件的衣服呢，是因为他害怕出现那种在《皇帝的新衣》里面出现的最后赤身裸体、什么衣服都没有穿的状况。我用这样的一个比喻来描述当时的这些编程语言太过复杂。而当时的编程太过复杂是因为每一个人都想往里面加更多的功能，最后就导致这些新的功能最后超出了程序的必要性。所以，我就觉得我们应该回到一个比较简单的状况，让编程语言不要那么复杂。我同时也说，一个程序的正确性要比在写程序的时候的难易程度更重要。我现在回想起来，我当时说这些话，可能有一点太过傲慢。

问题五：您对中国计算领域的印象如何？在未来的行业发展中，您觉得中国能承担一个什么样的角色？

托尼·霍尔：其实，除了微软公司在中国做的一些工作之外，对于中国的计算行业，我了解得非常少。但是我知道微软公司非常地重视它在亚洲的研究实验室，我们对在此地工作的这些人员以及他们所从事的工作有着极高的尊重。我和在中国学术界的计算机科学家们也有一些联系。在我看来，他们非常聪明，也非常有活力和动力，并且应该说是前景非常光明。我希望在未来，也就是我提出的这个可验证软件倡议方面，中国的科学家能够发挥一个很大作用。

问题六：是否能有一种理论来评估计算机语言？

托尼·霍尔：其实现在没有一个大家都接受的一个理论来评估一个语言，那么，在实践当中，选择语言的原因呢，往往和语言的实际质量之间并没有太大关联。说到实际质量，它涉及到受欢迎的程度、它的时尚性、可获得性，以及它的可熟悉性、兼容性等要素。但是这个问题是我非常感兴趣的，这也是最开始启动我在可验证方面工作的初衷。

在我看来，语言设计的目标应该是确保他能够使我们以简便的方法来写出那些正确的程序。与此同时，使得出错的概率变得更难。对于一种语言，根据它最后写出来的程序的正确性进行评估，应该是评测一个语言质量的科学准则。比如说，你花越长的时间来证明这个程序最后写出来是正确的，就说明你用的这个语言，是越不成功的，质量是越低。

问题七：未来计算机语言是否可以成为人类自然语言这样？

托尼·霍尔：一个受欢迎的语言应该说，它一直具备着成长性，因为使用这些语言的人会用这个语言来实现不同的目的。在这方面而言，其实计算机的语言和人类的自然语言是有区别的，因为人类的自然语言在成长的过程中会有一些词慢慢地就不用了，或者一些词会发生变化，或者这个语言的形式会发生一些变化，而在计算机语言的范畴之内是相反的。因为我们现在计算机必须得能够读懂上一代的计算机的语言，所以，我想正是因为计算机行业要求的兼容性，使得你前面说到的自然语言当中旧语言被剔除掉的可能不太可能会发生，那么语言其实是以更加复杂的方式在向前演进。

访谈人介绍

托尼·霍尔

微软剑桥研究院首席研究员。1980年图灵奖获得者。

托尼·霍尔于1956年在牛津大学获得一生之中第一个也是唯一的学位，专业是哲学、古典语言与文学（拉丁语和希腊语）。随后，他在英国皇家海军学习俄语，在牛津大学进行了为期一年的统计学研究，在莫斯科国立大学进行了为期一年的机器翻译研究。在莫斯科国立大学期间，他发布了著名的快速排序算法(Quicksort)。

这个经历使得他的兴趣转向计算机。1960年，他作为程序员加入Elliott Brothers公司，领导开发了经典编程语言Algol 60的早期编译器。由于其出色成绩，托尼·霍尔最终成为该公司的首席工程师和首席科学家。1968年，他被聘任为英国贝尔法斯特女王大学计算机科学系的教授并开始了学术研究生涯，主要研究领域包括编程理论、计算机程序的准确性验证。

1977年，他返回牛津大学并加入编程研究小组。在这里，他设立了与计算科学有关的多个本科与硕士学位。1999年在牛津大学退休后，托尼·霍尔加盟微软剑桥研究院，从事程序精确性领域的深入研究，以及此领域某些早期研究成果的应用工作。

他在科学与工程领域的成就得到了广泛认可：荣获图灵奖和京东奖；英国皇家学会会员；英国皇家工程院院士；意大利科学院院士；以及美国国家工程院院士。