本文来自微信公众号： 返朴 ，作者：陈清扬
英国计算机科学家托尼・霍尔（Tony Hoare）于2026年3月5日逝世，享年92岁。他是当代最具影响力的计算机科学家之一，其开创性的工作奠定了现代程序设计与形式化方法的基础。霍尔的一生，是与软件复杂性战斗的一生——为了理解复杂的程序，他发明了快速排序算法、提出霍尔逻辑等理论，这些成果深刻塑造了计算机科学的发展路径。斯人已逝，但他所发明的算法、他所构建的理论框架，早已融入现代计算世界的血脉，跳动在每一行追求简洁与正确性的代码之中。
过去几十年里，软件开发最大的成本之一就是“写代码”。程序员需要花费大量时间编写、调试和维护程序。而今天，借助大语言模型和各种Coding Agent，生成代码变得越来越容易，代码本身似乎不再稀缺。
然而，一个问题随之出现：如果代码越来越容易生成，那么谁来理解这些代码？谁来保证它们的正确性？谁来控制不断增长的软件复杂性？
事实上，这并不是一个新的问题。六十多年前，一位英国计算机科学家就已经开始思考类似的问题，他就是托尼・霍尔（Tony Hoare）。
图1托尼·霍尔（Tony Hoare，1934-2026）丨图源：wiki
对于很多计算机专业的学生来说，知道霍尔的名字，是因为他与两个著名成果联系在一起：快速排序（Quicksort）和霍尔逻辑（Hoare logic）。霍尔一生传奇，做出过许多重要成果。不过，回顾他的职业生涯，我们会发现看似分散的工作背后，其实贯穿着同一个主题：
当软件系统越来越庞大、越来越复杂时，人类如何保持对它的理解？如何保证程序依然正确？
霍尔的一生，正是与软件复杂性作战的一生。
人物小传
霍尔全名Charles Antony Richard Hoare，于1934年1月11日出生在当时的英国殖民地锡兰（今斯里兰卡），在那里度过了童年之后又搬回英国。霍尔先后在牛津龙校（Dragon School）和坎特伯雷国王学校（The King's School）完成了中学教育，后于1953年进入牛津大学莫顿学院读古典学。这是牛津大学最具代表性专业之一，有着悠久的历史传统；在本科期间，学生主要学习拉丁语、希腊语、哲学与逻辑（现代哲学）等。中学时代的霍尔便对数学感兴趣，在阅读了罗素关于数学基础和哲学的著作之后，又延伸出对于哲学的兴趣。可以看出，霍尔的早期学习生涯走的正是英国传统精英教育路线。
完成本科学位后，霍尔按当时规定在英国皇家海军服役两年。出于冷战时期军事需要，英国当时培养了大批精通俄语的士兵，凭借在古典学学习语言的基础，霍尔获得了学习俄语的机会（事后他认为，他的海军上尉叔叔从中也起到了作用）。他完成了基础军事训练，但因为严重晕船，他从未在海上过夜，也未参与军事行动。
服役结束后，出于想做一点更实际的事情，霍尔在牛津大学注册了一个统计学的研究生课程，他花了很大力气说服教授，证明自己拥有足够的数学基础，最终才获得了资格。这段经历让他后来教计算机的研究生课程时，总会对人文、语言背景的申请者格外包容。
在研究生期间，霍尔第一次接触到了计算机——那是一台水星计算机（Ferranti Mercury），由弗兰蒂公司（Ferranti）生产。这台重达1.1吨的商业电子管计算机使用的是一种名为AutoCode的编码系统。事实上，AutoCode被认为是一种早期高级编程语言，它的出现已经代表了编程生产力的一次跃迁——此前人们使用机器码进行编程，而在AutoCode中，可以使用常见的算术表达式，并且具备基本的循环等等。就这样，AutoCode成了霍尔掌握的第一门编程语言。他还在牛津旁听过数理逻辑大家王浩的课程，当时王浩用IBM 704计算机完成了《数学原理》（Principia Mathematica，罗素和怀特海的巨著）中诸多命题的自动证明。
在课程末期，霍尔作为交换生前往莫斯科国立大学学习。苏联数学大师柯尔莫哥洛夫在这里创建了著名的概率论教研室，霍尔便来到了这个概率论研究圣地。霍尔后来回忆写道：“我必须承认，在俄罗斯攻读研究生水平的概率论数学时，我感到力不从心。”
在机缘巧合下，霍尔收到英国国家物理实验室（National Physical Laboratory，NPL）的邀请，参与到一个俄语翻译英语的机器翻译项目中。正是在这次翻译项目中，霍尔提出了他最著名的工作之一——快速排序法。
访学临近尾声时，他又收到已从海军退役的叔叔来信——叔叔退休后正负责组织在莫斯科举办一个英国计算机展览会，邀请他担任俄语翻译。正是在这场展会上，他结识了埃利奥特兄弟公司（Elliott Brothers）的团队，对方不仅向他发出入职邀请，还邀他随团队一同返程，沿途协助处理俄语相关的海关事务。
回到英国后，霍尔在埃利奥特兄弟公司（Elliott Brothers）开始了他的编程生涯。他先是使用ALGOL 60实现并完善了快速排序算法，并将其发表；后面又主导开发了公司803计算机上的ALGOL 60编译器，该项目大获成功。霍尔因此受邀加入国际信息处理联合会（IFIP）的ALGOL工作组，共同参与设计ALGOL 60的继任编程语言。在当时的情境下，人们认为编程语言应该和硬件一样，每隔几年就升级一次。在会议讨论期间，霍尔和尼古拉斯・沃斯（Nicholas Wirth，1984年图灵奖得主）提交了ALGOL W的草案，不过遭到拒绝，委员会最终选择了一门十分复杂、具有众多特性的新语言。致力于追求简洁、提倡简化语言的霍尔在提交了少数派报告并遭到拒绝之后，没有再继续参加后续的会议。
1968年，霍尔离开了埃利奥特兄弟公司，来到贝尔法斯特女王大学任教，1977年又回到母校牛津大学。在大学的职业生涯期间，霍尔致力于程序正确性的研究，做出了诸如霍尔逻辑、通信顺序进程（Communicating Sequential Processes，CSP）等程序验证方面的奠基性工作。值得一提的是，霍尔曾与中国计算机科学家何积丰合作，提出程序语义的统一理论（Unified Theories of Programming）并出版著作。退休之后，霍尔继续在微软剑桥研究院担任研究员，活跃于学术界与工业界之间。
由于“对编程语言的定义和设计做出的基础性贡献”，霍尔获得1980年图灵奖，随后于1982年当选英国皇家学会院士，2000年因学术贡献被英国女王授予爵士头衔，同年获得日本京都奖。
2026年3月5日，霍尔逝世，享年92岁。他的一生几乎贯穿了现代计算机科学从萌芽到成熟的全过程，而他的研究也始终围绕同一个核心问题展开：如何让软件变得可以被理解、被描述，并最终被证明。
快速排序算法——分而治之
霍尔在苏联研究机器翻译项目时，当时的计算机存储容量极低，甚至只能存储一句话，翻译一个词就要读取一次磁带（词典存在磁带中）。为了更快完成，人们想到把句子中的单词按字母排序，这样一次读磁带就能完成整句的翻译。霍尔的任务就是在计算机上实现这个功能，为此他做了大量的调研，发表了人生第一篇学术论文——是用俄语写的。
机器翻译的工作也让霍尔开始思考排序问题。有一天，坐在房间里的沙发上，他想到了一种新的排序方法：找准一个基准之后，把小于它的数都放在左边，大于它的数都放在右边，这样就把一个大的排序问题拆分成两个排序子问题，再分别对左右两边的子序列进行排序即可，这便是快速排序的思想。霍尔当时使用了他唯一知道的编程语言AutoCode进行了理论上的尝试（由于保密，他甚至没有见到苏联的计算机），同时他也必然地碰到了一个问题：当时AutoCode并不支持递归，而递归正是快速排序算法最自然的表达方式。这个问题直到霍尔两年后接触到ALGOL 60才解决，ALGOL 60的递归设计让他大为惊叹。下面简要介绍快速排序算法思想。
假设我们要排序下面这组数字：
[7,2,9,1,5,8,3]
快速排序先选择一个基准元素（pivot）。为了简单起见，我们选择第一个元素7。
下面的步骤非常关键：把所有小于7的数字放到左边，把所有大于7的数字放到右边。
小于7：[2,1,5,3]
大于7：[9,8]
经过一次这样的“划分”（partition）之后，数组变成了：
[2,1,5,3]7[9,8]
此时7已经处在最终正确的位置上：它左边的数都比它小，右边的数都比它大。剩下的问题变成：
对左边的[2,1,5,3]和右边的[9,8]分别再做同样的操作。
例如，对左边部分继续选择2作为基准：
小于2：[1]
大于2：[5,3]
于是得到：
[1]2[5,3]
再继续递归处理[5,3]和右边的[9,8]，最终整个数组会变成：
[1,2,3,5,7,8,9]
这就是快速排序的核心思想：每次选一个基准，把问题拆成两个更小的子问题，然后递归地解决它们。
快速排序的核心优势在于它是一种原地排序算法，不需要额外的数组保存中间结果，它采用“比较大小”和“交换”的方式对元素进行位置调换，从而完成排序。这极大地节省了宝贵的内存空间，无论是在当时的早期计算机，还是在现在的计算机，这样“原地排序”的方式，都可以高效地运行。
快速排序算法的问世，还有一个有趣的六便士故事。霍尔加入了埃利奥特兄弟公司后，告诉他的上司，自己发明了一种比当时流行的希尔排序还要快的算法。他的上司对此表示怀疑，甚至和他打赌六便士。然而，当上司亲自在机器上实现了快速排序，并且发现它的确比他此前使用的归并排序明显更快后，便坦然认输，信守承诺支付了这六便士。
快速排序算法发表后迅速被广泛采用，成为计算机科学的经典算法。值得一提的是，其思想天然也蕴含了一个姐妹算法，即快速选择（quick select），可以在线性时间内解决选择问题：从一个给定的数组中选择第k大的元素。每次通过基准拆分成两个子问题以后，如果只对其中一个子问题进行排序，即可得到快速选择算法。
从成功到失败：复杂性的代价
在埃利奥特兄弟公司，霍尔主导开发的第一个大项目是一个ALGOL 60编译器。ALGOL 60可以说是现代高级编程语言的鼻祖，C、C++、Java等现代编程语言均借鉴了其思想与语法。直至今日，算法教科书——譬如《算法导论》中的伪代码——依然使用类似ALGOL 60的语法。ALGOL全名Algorithmic Language，顾名思义，它是一种专门用来表达算法的编程语言。
研发期间，霍尔秉持了若干原则，使得其团队取得了巨大成功，其中包括著名的“动态数组下标检查”：即在编译数组访问A[i]时，编译器会自动插入边界检查代码，以确保在程序运行时检查索引i是否越界。这对于如今的高级编程语言早已成为标配，但在当时的编程语言中可谓是开了先河。后来霍尔团队发现，尽管这样的动态检查会降低程序运行的性能，但是客户却无一例外地强烈要求保留这个特性。这个原则再次印证了霍尔的软件工程思想：正确性是最重要的，而不在于代码能够跑得有多快。
在ALGOL 60编译器取得成功之后，霍尔和他的团队更加雄心勃勃。他们认为，他们不仅能够开发一个编译器，还能够为公司的下一代计算机构建完整的软件生态。当时，埃利奥特兄弟公司正在推出性能更强大的Elliott 503计算机。相比上一代的803计算机，503在软件兼容的同时运算速度还要快70倍。为了支持更复杂的应用场景，公司为其配置了大量外设，包括读卡器、行式打印机、磁带驱动器，甚至还配备了一种容量更大但速度慢得多的磁芯后备存储器（Core Backing Store）。
为了充分发挥这些硬件能力，公司决定开发一整套系统软件，项目被命名为Elliott 503 Mark II。与此前专注于一个ALGOL编译器不同，这一次团队试图同时解决几乎所有问题：新的汇编器、自动管理内存覆盖的运行时系统、统一的输入输出框架、文件系统与作业控制工具、完整实现的ALGOL 60编译器，以及FORTRAN编译器。今天看来，这几乎相当于同时开发操作系统、运行时环境、文件系统和多个编译器。
读到这里，有经验的软件开发者大概已经能闻到危险的气息。随着开发推进，问题开始逐渐暴露。等到系统逐渐成形时，团队才发现，整套软件几乎已经占满了计算机全部内存，甚至没有剩余空间供客户运行自己的程序。而且由于硬件寻址长度的限制，增加内存根本不可能。霍尔后来回忆说，团队为各种功能制定了详细计划，却忽略了一个最基本的问题：这些软件究竟需要占用多少内存。
更糟糕的是，为了弥补主存不足，系统不得不频繁在主存与速度慢15倍的后备存储器之间交换数据，产生了今天所谓的“抖动（thrashing）”现象。最终交付出来的ALGOL编译器运行速度竟然只有每秒几个字符。经过多次延期和抢救之后，公司不得不做出决定：整个Elliott 503 Mark II项目被彻底取消。超过30人年的开发工作付诸东流。
这次失败对霍尔产生了极大的冲击。他后来意识到，问题并不在于程序员不够聪明，而在于系统的复杂程度已经超出了团队能够理解和控制的范围。多年以后，他在图灵奖演说中总结出了那句广为流传的话：
“软件设计有两种方法。一种是把系统设计得如此简单，以至于明显没有缺陷；另一种是把系统设计得如此复杂，以至于没有明显缺陷。”（There are two ways of constructing a software design:one way is to make it so simple that there are obviously no deficiencies,and the other way is to make it so complicated that there are no obvious deficiencies.）
这句略带幽默的话背后，凝结着这一次代价高昂的失败经历。对于霍尔而言，503项目的崩溃成为他此后数十年研究工作的一个重要转折点。他开始思考：如果软件复杂性终将失控，人们是否能够找到更系统的方法去理解、验证和管理程序？后来他关于程序验证、并发程序以及CSP等许多研究，都可以看作是在寻找这个问题的答案。
数学家可以证明定理，程序员能不能证明程序？
20世纪60年代，随着硬件计算能力的逐渐增长，软件也随之变得越来越复杂。各种软件问题开始层出不穷：难以交付、代码质量降低，乃至混乱到难以维护。霍尔遇到的失败，其实并非个例。以至于到了1968年，北大西洋公约组织（NATO）专门召开了一次会议来探讨“软件危机”（software crisis）。同年，霍尔离开了埃利奥特兄弟公司，加入了贝尔法斯特女王大学，在大学里，他开始思考程序正确性的问题。
当时，人们主要依赖测试和经验来保证程序正确性。写完程序之后运行几个例子，比如输入1，结果正确；输入10，结果正确；再同样尝试几次都正确，便认为程序大概没有问题。然而这种经验方式有一个本质问题，无论测试多少次，都只能说明程序在这些特定情况下表现正常，而无法证明它在所有情况下都正确。这也是为什么埃德斯格・迪杰斯特拉（Edsger Dijkstra，1972年图灵奖得主，同时也是霍尔的好朋友）曾一针见血地说道：“程序测试可以用来发现bug，但永远无法证明错误不存在。（Program testing can be used to show the presence of bugs,but never to show their absence.）”
与此同时，霍尔也在思考：数学家可以通过公理和演绎推理来证明一个定理，程序员是否也可以通过定义公理和逻辑推导来证明一个程序的正确性？
一天，霍尔偶然翻到了鲍勃・弗洛伊德（Bob W.Floyd，1978年图灵奖得主）发表的一篇论文“Assigning Meanings to Programs”。这篇论文提出了一种基于程序流图证明程序正确性的方法。霍尔大受启发，随后泛化了弗洛伊德的方法，使得它可以直接对代码本身进行推理，而不再需要流图这样的表示形式，这大大提高了程序证明的实用性。霍尔由此提出的霍尔三元组（Hoare triple），现在已成为程序验证课堂和教科书上的标准符号（notation）。其形式如下：
P{Q}R
它的意思是，如果在程序Q运行前，条件P成立，那么在Q完成执行以后，条件R也成立。这是一种简单有效的标记符号，基于这个符号，霍尔定义了一系列的公理系统。下面我们通过一个简单的例子，来看如何使用霍尔逻辑证明程序的正确性。
前置条件（P）：x为正整数
程序（Q）：
if x>1 then
x=x+1
else
x=x*3
后置条件（R）：x>2
现在的问题是，假设前置条件P成立，那如何证明当Q运行结束以后，后置条件R也一定成立？
霍尔逻辑的思路是采用反向推理：如果Q完成运行后需要R成立，那P最少需要满足什么条件？程序有两个分支，需要分开证明，即当两个分支的反向推理证明都正确，才能推导出最终的结果正确。
先看第一个分支then，这里唯一的语句是一个赋值语句x=x+1。霍尔逻辑的思路是，如果要运行x=x+1之后x>2成立，那运行之前，x需要满足什么条件？这里的方式就是用x+1替换x>2中的x，得到x+1>2，即x>1；显然，这正是这个分支的前置条件本身。
再看另一个分支else，这里的赋值语句是x=x*3。还是一样的办法，使用x*3替换x>2中的x，得到x*3>2，即x>2/3。这个分支的前置条件是“x为正整数且x≤1”，即x=1，显然，这是x>2/3的充分条件。
由此，两个分支都已被分别证明，于是我们可以推导出P{Q}R。注意这里霍尔逻辑还蕴含另一种思想：它只处理程序语言层面的语义，譬如变量、语句赋值、条件跳转，还包括循环等等，而假定更下一层的数学层面的逻辑已经被处理，如上文例子中将x+1>2简化为x>1。这就是计算机科学里常谈到的抽象——一个层面不需要知道或处理另外一个层面的问题。霍尔逻辑负责的是程序语义的层面，数学逻辑交给下一层来处理；而下一层的数学逻辑也不需要管上层的计算机程序层面。
通过霍尔逻辑，计算机程序变得直接可推导、可证明，而不再仅仅是与硬件绑定的附属品、一种手工艺活。霍尔逻辑第一次给程序建立了一套简洁而系统的形式化推理体系，使程序正确性的证明成为可能，也深刻影响了后来形式化验证的发展。
再简单一提的是，这里谈到的程序是串行的单个程序。进入1970年代，随着多道程序和多处理器系统的发展，并发程序的正确性开始成为计算机科学的重要研究课题。当计算机上有多个程序同时在运行，它们之间共享着数据，可能同时对数据进行操作，如何还能保证操作的正确性？当时主流的并发程序大多采用共享内存模型，通过锁、信号量等同步机制来保证程序的正确性。在这样的背景下，1978年霍尔提出通信顺序进程（CSP）——一种全新的并发程序设计范式，再一次地开了先河：程序（或进程）之间不通过共享状态进行通信，而是通过消息通信来协作，每个进程只维护自己的局部状态。这一思想深刻地影响了三十年后Go语言的设计。其设计箴言之一便是：Don't communicate by sharing memory;share memory by communicating。也就是说，不要让多个线程共同操作同一份数据，而应通过发送消息来转移数据的所有权。
十亿美元的错误，还是对“简单”的务实妥协？
霍尔与复杂性的对抗，并不总是意味着追求纯粹的数学完美。有时，真正的工程智慧恰恰体现在一种务实的妥协中。这就不得不提到霍尔职业生涯中颇具争议的一段轶事——关于“空引用（Null Reference）”的引入。
前文提到，霍尔与尼古拉斯・沃斯设计了一门优雅的语言ALGOL W。ALGOL W在语言层面引入了两种新特性：记录（record）和引用（reference）。记录就类似于C语言的结构体（struct），可以表示复合类型的数据结构；而引用则相当于指针，可以指向一个具体的记录实例。记录和引用的引入，可以大大提高代码的抽象程度，但这两项新特性的引入也带来了一个问题：当一个引用还未指向某一个特定记录的时候，它的值应该是什么？
在设计类型系统时，霍尔面临着一个棘手的工程抉择。
如果要求语言在类型系统上做到绝对的安全与一致性（coherent），编译器就必须在编译期严格保证每一次引用都必然指向一个合法的记录。否则，即便是在今天，这种对形式上“完美”的追求，也会不可避免地导致语言规范和编译器的极度复杂化，甚至会让程序员在日常开发中陷入为了满足类型检查而编写繁琐代码的泥潭。
面对理论完美与系统复杂性之间的冲突，霍尔做出了一个决定：他选择在语言中引入“Null”，即空引用。用一个特殊的Null值来表示“这个引用当前没有指向任何东西”，是一个顺其自然且极其轻量的机制。霍尔后来回忆时坦言，这样做“仅仅因为它实现起来太容易了”。在当时的条件下，他选择接受一个运行时的微小风险，换取了编译器实现和基础语言设计的极大简化。好友迪杰斯特拉（Edsger W.Dijkstra，1972年图灵奖得主）也曾用一个十分形象的比喻提醒过霍尔：
“如果你引入了Null引用，那么你的程序中的每一个单身汉对象都看起来和同一个人结婚了，这个人就是Null。”
后来发生的事情，今天的程序员已经非常熟悉。随着后世面向对象编程语言（如C++、Java）的普及，Null引用被作为一种标准设计广泛继承。由于缺乏强制的空值检查，它成为无数Bug、系统崩溃（著名的NullPointerException）甚至安全漏洞的根源。
2009年，75岁的霍尔在一次演讲中公开为此道歉，戏称这是自己当年为了贪图实现简单而造成的“十亿美元错误”（Billion-Dollar Mistake）。后来许多技术文章常常以此来批判Null的设计。但实际上，从1960年代的技术背景来看，计算机内存、后备存储空间都极其有限，引入一套“完美”却繁琐的类型系统会让程序员编程以及编译器的实现都变得非常复杂。引入Null引用，其实并非一个简单的“错误”，甚至可以说是相当合理的折中（trade-off）。这也恰恰印证了霍尔对抗复杂性的哲学的另一面：宁可接受一个简单、直接且有明确边界的缺陷，也不要为了追求形式上的完美而陷入无法理解的复杂。
随着编程工具的逐步发展，静态分析对代码的补全，以及使用AI工具的补全，再到如今越来越多代码由AI直接生成，最佳的工程实践似乎又在随着技术的变化而变化。以前，人工地去声明一个引用“可能为空”，并且让它通过所有的类型检查，的确相当繁琐。而现在，程序员更多是一种架构师的角色，“编程”复杂性的负担正在不断降低，而这种严谨而繁琐的类型系统反而给AI套上了更严格的规范，提高了程序的正确性。
结语
回顾托尼·霍尔的一生，人们很容易记住几个具体成果：快速排序、霍尔逻辑、CSP等。而这些成果背后，隐藏着一个更深层的主题：无论是设计优雅的排序算法，还是试图证明程序正确性，抑或反思大型软件系统的失败经验，霍尔始终在与同一个敌人作战——复杂性。技术会不断变化，编程语言会更新换代，人工智能也将继续改变软件开发方式。但对于简单性、正确性和可理解性的追求，却永远不会过时。这或许正是霍尔留给计算机科学最重要的遗产。
参考文献
[1]C.A.R.Hoare.An Axiomatic Basis for Computer Programming,Communications of the ACM,1969
[2]Bob W.Floyd.Assigning Meanings to Programs,Proceedings of Symposia in Applied Mathematics,1967,19,19–32.
[3]Communications of the ACM.In Memoriam:C.A.R.Hoare.2026-03-16.https://cacm.acm.org/news/in-memoriam-c-a-r-hoare/
[4]Tony Hoare.Null References:The Billion Dollar Mistake.InfoQ 2009-08-11.https://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare/
[5]Tony Hoare."Oral History of Sir Antony Hoare." Interview by Jonathan P.Bowen.Transcript,September 8,2006.Computer History Museum,Reference no.X3698.2007.http://archive.computerhistory.org/resources/text/Oral_History/Hoare_Sir_Antony/102658017.05.01.pdf.
[6]C.A.R.Hoare.The Emperor’s Old Clothes（1980年图灵奖演讲）.Communications of the ACM,1981.https://worrydream.com/refs/Hoare_1981_-_The_Emperors_Old_Clothes.pdf
[7]Jones,Cliff."Antony Hoare Interview." Transcript,2015-11-24,ACM A.M.Turing Award Oral History Project.https://amturing.acm.org/pdf/HoareTuringTranscript.pdf.
[8]Bertrand Meyer,Celebrating Tony Hoare’s mark on computer science,https://bertrandmeyer.com/2026/03/16/celebrating-tony-hoares-mark-on-computer-science/
[9]Tony Hoare,Stories from a Life in Interesting Times（2000年京都奖演讲）.
[10]Tony Hoare，My Early Days at Elliotts，2008 at the Science Museum in London.