Tony Hoare 在 3 月 5 日去世了。

他的全名是 Charles Antony Richard Hoare，计算机科学界里少数真正能说"改变了整个行业的走向"的人之一。他 90 岁，图灵奖得主，英国皇家学会院士，被封爵。用了七十年时间研究如何把程序写对，让程序可以被证明是正确的。

然而他留给大众记忆最深刻的，是一个他后悔发明的东西。

Quicksort 与空引用

1959 年，Hoare 在莫斯科做访问学者。他需要把一批俄语单词排序，用卡片手工实现。为了提高效率，他发明了一个算法：选一个基准值，把小的放左边，大的放右边，对两侧递归重复。这就是 Quicksort。

如果你用过任何编程语言，你用过 Quicksort，或者基于它改进的变体，很可能数千次。半个世纪后它仍然是最广泛使用的排序算法之一。

1965 年，Hoare 在设计 ALGOL W 时加入了空引用。他后来在 2009 年的一次演讲里说：

"我把它叫做我的十亿美元错误。1965 年，我在设计第一个面向对象语言 ALGOL W 的引用类型系统时发明了空引用。我的目标是确保所有引用的使用都绝对安全，由编译器自动检查。但我没能抵挡住加入空引用的诱惑，仅仅是因为它太容易实现了。这导致了无数错误、漏洞和系统崩溃，在过去五十年里造成了数十亿美元的痛苦和损失。"

这个"十亿美元错误"的表述在软件工程界广泛流传，已经成为一个标准引用。Null pointer exception、segmentation fault、空指针解引用——这些是几乎每个程序员都遇到过的噩梦，Hoare 说它们源于他 1965 年一个为了方便的决定。

后来的语言——Rust、Kotlin、Swift、Haskell——在类型系统里用不同方式强制要求显式处理"值可能不存在"的情况，消除了大量空引用相关的 bug。这些设计，某种程度上是在为 1965 年的那个决定付账。

CSP 和并发思维

如果说 Quicksort 是 Hoare 最广为人知的工程贡献，那么他真正引以为傲的工作可能是 CSP——Communicating Sequential Processes，通信顺序进程。

1978 年的那篇论文，以及 1985 年出版的同名书，提供了一套用数学语言描述并发系统的方法：多个进程，各自独立运行，通过显式通信（发送和接收消息）同步，而不是共享内存。这套思想后来直接影响了 Go 的 goroutine 和 channel 设计，影响了 Erlang 的 actor 模型，影响了 Clojure 的 core.async，影响了整整一代并发编程语言的走向。

Go 团队的 Rob Pike 和 Ken Thompson 在多个场合提到 CSP 是 Go 并发模型的直接来源。那句常被引用的 Go 格言——"不要通过共享内存来通信，而是通过通信来共享内存"——是 CSP 思想的口语化表述。

Hoare 逻辑：程序可以被证明正确

还有第三件事值得记。

1969 年，Hoare 发表了一篇短文，提出了一套用来形式化推理程序正确性的逻辑系统，后来被称为 Hoare 逻辑或者 Floyd-Hoare 逻辑。基本思想是：用前置条件和后置条件包围一段代码，证明如果前置条件成立，代码执行后后置条件也会成立。

这是软件形式化验证的基础。今天的 Coq、Lean、Isabelle，以及 AWS 用 TLA+ 验证分布式系统正确性，以及 seL4 这个被数学证明正确的微内核操作系统——都生长在 Hoare 逻辑奠定的地基上。

形式化验证在工程实践里仍然是小众工具，但在安全攸关系统（航空、医疗、核能）里已经是标准配置。Hoare 用了一生来推进"程序可以被证明是正确的"这个信念。

关于那个后悔

Hoare 那句"十亿美元错误"在流传过程中有时被过度戏剧化了，好像他对自己的整个职业生涯悔恨交加。事实并非如此。他对空引用的后悔，是一个严肃的技术人对一个可以做得更好的决策的坦诚——那个决策让了便利，牺牲了安全。

这种坦诚本身就是一种罕见的品质。技术圈里并不缺少把自己的每个决策都事后合理化的人，也不缺把"我当时不知道"当成万能借口的人。Hoare 在 2009 年，已经是图灵奖得主、已经名满天下，选择站在公开演讲里说：那是我的错，它造成了巨大的损失，我为此后悔。

一个能说出这种话的人，值得被认真记住。