托尼·霍尔 — 先驱 — 计算机科学

1960 年，一位 26 岁的英国年轻人为了和上司打的一个赌，写出了一种排序方法。它快得不可思议，至今仍是计算机每天排序数据时最常用的算法之一。但写出它的查尔斯·安东尼·理查德·霍尔（C. A. R. Hoare，人称 Tony Hoare），后来用一生做的，是一件更难的事：让我们相信一个程序真的是对的。

破除误解：他最重要的贡献不是快速排序

提到霍尔，几乎所有人首先想到"快速排序（Quicksort）"。这确实是天才之作，但若只记住这一点，就错过了他更深远的事业。

霍尔真正的一生主题是程序正确性：我们凭什么敢说一段代码"没有 bug"？在他之前，程序对不对主要靠测试——跑一跑、看看有没有出错。霍尔想要的是数学级别的确定性：像证明几何定理那样，证明一个程序对所有输入都会给出正确结果。快速排序是他的成名作，霍尔逻辑才是他的毕生工程。

现场：为一个赌打出的快速排序

1959 年，霍尔在莫斯科国立大学学习机器翻译，需要把词典里的词排序以便查找。他想出一个递归的点子：随便挑一个"基准"元素，把比它小的扔到左边、比它大的扔到右边，再对左右两堆分别重复同样的操作。

他和上司打赌，说自己能想出比当时通用方法更快的排序——上司帕特·沙克尔顿（Pat Shackleton）赌六便士说他做不到，结果输了。1960 年霍尔回到英国，加入 Elliott Brothers 公司，把这套想法实现出来——这就是快速排序。它的平均时间复杂度是 $O(n \log n)$ ，且常数因子小、原地排序、对缓存友好，因此在实践中往往跑赢理论上"更稳定"的对手。六十多年过去，它仍是各种标准库排序的核心组件之一。

这个"分两边"的一步叫分区（partition），它的正确性靠一条不变量保证：扫描过程中始终维持"左边指针之左的元素都不大于基准、右边指针之右的元素都不小于基准"。只要这条不变量在每次迭代后都成立，循环结束时基准必然落在最终位置上——左堆全在它左边，右堆全在它右边。用不变量论证正确性，而不是"跑几个例子看看"，这个思维习惯贯穿了霍尔的一生：快速排序里已经藏着霍尔逻辑的胚胎。

平均复杂度 $O(n \log n)$ 的直觉也不难看清：只要分区大致对半，递归深度就是 $\log n$ 层，每层所有分区合起来只扫过 $n$ 个元素。它真正的快还有工程原因：分区是顺序扫描，对缓存极其友好，而且不需要额外的存储空间。

但快速排序有个著名的脾气：最坏情况下（比如基准选得很糟）会退化到 $O(n^2)$ 。如何选基准、如何防止被恶意构造的输入拖垮，至今仍是工程实践中的经典话题——这本身就说明，一个"看起来对"的算法，离"在所有情况下都好"还有多远。

代价：一次价值三十人年的失败

在 Elliott 的八年里，霍尔并不只有成功。他先是带领一个小团队（成员包括他的妻子吉尔）为 Elliott 803 写出了最早的 ALGOL 60 编译器之一，相当成功；但随后他为 Elliott 503 主持设计的 Mark II 操作系统，功能定得雄心勃勃、项目管理失控，最终被整个放弃——超过三十人年的编程工作量付诸东流。

这次失败比成功更深刻地塑造了他。1980 年，他在图灵奖演讲《皇帝的新衣》（The Emperor's Old Clothes）里公开复盘了这段经历，得出的结论朴素而严厉：一个设计如果复杂到没人能完整理解，它就不可能可靠。软件可靠性的前提不是更多的测试，而是设计本身简单到可以被证明。

1968 年，他离开工业界，出任贝尔法斯特女王大学计算科学教授；1977 年转赴牛津大学主持编程研究组（Programming Research Group），直到 1999 年退休。霍尔逻辑与 CSP，都是这三十余年学术生涯的产物。

核心：霍尔逻辑——给程序做证明

1969 年，霍尔发表《计算机程序设计的公理基础》，提出了后来被称为"霍尔逻辑（Hoare Logic）"的形式系统。它的核心是一个三元组：

$\{P\}\ C\ \{Q\}$

读作：如果在执行程序片段 $C$ 之前，条件 $P$（前置条件）成立，那么执行之后，条件 $Q$（后置条件）必定成立。

这个简单的记号威力惊人。它把"程序是否正确"变成了可以逐行推演的逻辑问题：给每条语句配一条推理规则（赋值、顺序、条件、循环……），就能像做数学证明一样，从前置条件一步步推到后置条件。循环正确性的关键工具——"循环不变量"（loop invariant），也由此被系统化。

看两条规则就能领会它的结构。赋值语句的公理是：

$\{P[E/x]\}\ x := E\ \{P\}$

意思是：若"把 $P$ 中的 $x$ 替换为表达式 $E$"在执行前成立，则执行 $x := E$ 之后 $P$ 成立——注意推理是倒着走的，从想要的结果反推执行前必须满足什么。循环的规则则说：若存在断言 $I$（循环不变量），使得"在循环条件成立时执行循环体仍保持 $I$"可证，那么整个循环结束后 $I$ 依然成立。找不变量，本质是回答"这个循环每一步究竟在维护什么"——这正是程序员写循环时脑子里应该有、却常常说不清的东西。

还要留意一个边界：三元组保证的是部分正确性——若 $C$ 终止，则结果满足 $Q$；它不保证 $C$ 真的会终止。证明终止需要另外引入一个每轮严格递减的"变体"（variant）。"正确"与"终止"分开处理的分工，此后成为整个程序验证领域的标准做法。戴克斯特拉（Edsger Dijkstra）在此基础上发展出"最弱前置条件"（weakest precondition）演算，把这套逻辑变成了可机械推导的程序设计方法。

为什么这件事重要？因为测试只能证明"在我试过的这些输入上没出错"，永远无法穷尽所有输入；而霍尔逻辑提供了一条原则上的道路，去证明"对所有满足前置条件的输入都正确"。今天的程序验证工具、契约式编程（如 Eiffel 的前置/后置条件）、乃至形式化验证的整个领域，都站在霍尔 1969 年这篇论文的肩膀上。

CSP：如何谈论"同时发生的事"

1978 年，霍尔提出通信顺序进程（Communicating Sequential Processes, CSP），一种描述并发系统的数学语言。它的核心思想是：与其让多个进程共享内存、再用锁去保护（极易出错），不如让进程各自独立、只通过消息通道（channel）通信。

这个思想极其有影响力。Occam 语言、以及后来 Go 语言的并发模型（"不要通过共享内存来通信，而要通过通信来共享内存"），都是 CSP 思想的直接后裔。在并发 bug（竞态、死锁）层出不穷的世界里，CSP 提供了一套能被严格推理的并发语义——这又回到了霍尔毕生的执念：让正确性变得可证明。

CSP 的通信还有一个关键设计：消息传递是同步的——发送方与接收方必须同时就绪，像两个人当面交接一件物品，没有缓冲区代为暂存。这个看似不便的限制换来语义的干净：通信事件本身成为系统行为的基本单位，进程间的交互可以写成一套代数等式，用来做等价推理与死锁分析。沿着这条路线，牛津团队后来做出了模型检测工具 FDR，CSP 由此成为少数"既能写规格、又能机器检验"的并发理论之一。

值得一提的是，霍尔在并发上的贡献并不止于 CSP。早在 1974 年，他就提出了管程（monitor）这一操作系统级的同步抽象：把共享数据和操作它的过程封装在一起，由编译器和运行时保证同一时刻只有一个进程能进入管程，并配以条件变量来挂起/唤醒进程。今天 Java 的 synchronized、各种语言的内置锁与条件变量，本质上都是管程思想的实现。事实上，他的图灵奖正式授予理由，表彰的是"在编程语言的定义与设计方面的根本性贡献"——快速排序、霍尔逻辑、CSP、管程，是同一种追求的不同侧面。

代价与争议：价值十亿美元的空引用

1965 年，霍尔在设计 ALGOL W 语言时引入了"空引用"（null reference）——一个表示"这里什么都没有"的特殊值。他后来坦言，这么做"仅仅因为它太容易实现了"。

2009 年，在伦敦 QCon 大会上，已是泰斗的霍尔公开为此道歉，称之为"我价值十亿美元的错误"（my billion-dollar mistake）。他的理由是：空引用导致了无数的崩溃、漏洞和系统故障——任何对象都可能"是 null"，而忘记检查就会在运行时炸掉。这半个多世纪里因 null 造成的损失，他估计"或许已达十亿美元"。

这个反思深刻地影响了后来的语言设计：Rust 用 Option 类型、Kotlin 用可空类型标注、Haskell 用 Maybe，都是为了在编译期就堵住 null 这个漏洞，把"可能没有值"这件事变成类型系统里必须显式处理的情况。一个 1965 年图方便的决定，成了几代语言设计者引以为戒的教训——这本身正是霍尔式诚实的体现：连自己最大的失误也拿出来，作为推进学科的反面教材。

霍尔 1980 年获图灵奖。他于 2026 年 3 月去世，享年 92 岁。

跨域连接

公理：给每种语句配一条推理规则，"程序正确"就变成从公理出发的推导。要害在于规则必须与语言的语义严格一致——一旦语言加入别名或副作用，原有规则不再可靠，必须重新证明。这条要求一次性解释了形式化为什么在指针与并发面前变难：难的不是证明，是先得有一套还站得住的规则。
联邦制：通信顺序进程的取舍是把状态分散到各自主体，只允许通过明确定义的通道交互。好处是局部出错不污染全局，代价是需要显式协议和更多往返。推论也就跟着出来：交互频繁且延迟敏感时，集中共享反而更划算——这正是共享内存并发在高性能场景里始终没被取代的原因。
模态逻辑：空引用的问题在于它让每个类型实际上都变成了"该类型或者没有"，却不把这层可能性写进类型里。后来用可选类型把它显式化，与模态逻辑把"可能"提升为算子、从而能对它做推理，是同一手法。收益不是复杂度减少，而是把隐含情形挪到了能被机械检查的位置。
博弈论：快速排序的平均情况分析预设了输入分布，而攻击者可以自己挑分布——把输入看成对手的选择，平均保证立刻失效。随机化枢轴的作用正是把随机性从"假设输入随机"搬到"算法自己掷骰子"，于是保证不再依赖对手是否配合。这是把一个统计论证改造成博弈论证的经典一步。
形式化方法与验证：他给出的是原则上的路径，实用化卡在两处：循环不变量要人来提供，而规格本身也可能写错。工业界因此普遍只做部分验证——挑最关键的性质证明，其余仍交给测试。收益规律也随之清晰：与被验证性质的严重性成正比，与代码规模成反比。

参考文献

Hoare, C. A. R. Quicksort. The Computer Journal 5, no. 1 (1962): 10–16.
Hoare, C. A. R. An Axiomatic Basis for Computer Programming. Communications of the ACM 12, no. 10 (1969): 576–580.
Hoare, C. A. R. Communicating Sequential Processes. Communications of the ACM 21, no. 8 (1978): 666–677.
Hoare, C. A. R. Null References: The Billion Dollar Mistake. QCon London (2009). （会议演讲，InfoQ 存有完整录像与文字稿）

破除误解：他最重要的贡献不是快速排序#

现场：为一个赌打出的快速排序#

代价：一次价值三十人年的失败#

核心：霍尔逻辑——给程序做证明#

CSP：如何谈论"同时发生的事"#

代价与争议：价值十亿美元的空引用#

跨域连接#

参考文献#

延伸阅读#