那个制造了"十亿美元错误"的天才，走了
Tony Hoare 去世了。
3月5日。消息由他的学生、计算机科学家 Jonathan Bowen 确认，发布在法国博主 Aredius44 的 Blog 上。没有铺天盖地的讣告，只有几行简洁的法语，和一串 Wikipedia 链接。
但这个名字背后，藏着现代软件世界的地基，也藏着一个巨大的讽刺：他发明了计算机科学史上最著名的 Bug，又穷其一生试图消灭 Bug。
快速排序 vs 十亿美元错误：天才的两面
大多数人认识 C.A.R. Hoare（后来大家叫他 Tony），是因为教科书里那几行优雅的递归代码。
1962 年，他发明了快速排序（Quicksort）。分而治之，简洁如一把手术刀。这是计算机科学史上被运行次数最多的算法之一，支撑着你每天刷的短视频、搜的关键词、银行转账的流水。
但让他真正"出圈"的，却是一个道歉。
"我称之为我的十亿美元错误。1965 年，我发明了空指针（null pointer）。"
这个设计让无数程序在运行时突然崩溃，产生了难以计数的漏洞和安全事故。Hoare 晚年多次公开忏悔，说当时只是图方便，没想到这个"临时决定"成了全球软件业的噩梦。
有意思的是，他一边制造了混乱，一边又试图建立秩序。
不只是算法，是思维的语法
如果 Hoare 只写了快速排序，他只是个优秀的工程师。但他改变了我们思考软件的方式。
1972 年，他与 Dijkstra、Dahl 合著《Structured Programming》，给混乱的代码世界带来了结构化的曙光。1985 年，《Communicating Sequential Processes》（CSP）出版——这本书奠定了现代并发编程和分布式系统的理论基础。Go 语言的 goroutine，Erlang 的 actor 模型，骨子里都流淌着 CSP 的血。
更重要的是 Hoare Logic。这是程序验证的基石，让数学证明和代码执行第一次有了严谨的对应关系。没有它，今天的形式化验证、安全关键系统（飞机、高铁、核电站的控制软件）都无从谈起。
一位 Hacker News 上的评论者说得好："他的贡献横跨日常编码、算法设计和核心系统架构，很少有计算机科学家能覆盖这么广的维度。"
未竟的战役：当梦想输给现实
但 Hoare 有个遗憾。
他毕生致力于让形式化验证（Formal Methods）成为软件开发的标配——用数学证明程序没有 Bug，而不是靠测试碰运气。这个梦想至今未能实现。
正如一位网友在评论中写道："Sad that his (and many others') dream of widespread formal verification of software never came true."（令人悲伤的是，他（和其他许多人）让软件广泛实现形式化验证的梦想从未成真。）
这让人想起 Dijkstra 的担忧——那位同样是巨人的计算机科学家曾害怕自己只会被记住"最短路径算法"，而不是他关于编程本质的深刻思考。
Hoare 似乎面临着同样的命运：人们记得 Quicksort，记得 null pointer 的笑话，却很少有人读他关于 CSP 的论文，或者用 Hoare Logic 去证明一段代码的绝对正确。
尾声：我们还在用他的逻辑思考
说实话，软件行业今天依然活在 Hoare 的影子里。
当你写下一行 if (ptr != NULL)，你在处理他的"错误"；当你打开一个并发程序，你在用他的 CSP 模型；当你听到"形式化验证"这个词，那是他四十年前就在鼓吹的信仰。
他走了，留下了十亿美元的教训，也留下了试图修正这个世界的数学武器。
问题是：我们准备好用更严谨的方式写代码了吗？还是继续在他的"错误"和"修正"之间反复横跳？
【kimi-k2.5锐评】：一位靠"道歉"出圈的图灵奖得主，用一生证明了计算机科学最残酷的真相——制造问题的人，往往也是最想解决问题的人，但行业只想要快速排序，不想要形式化验证。
参考链接：
http://lefenetrou.blogspot.com/2026/03/in-memoriam-tony-hoare.html