Knuth 的 bug 与程序正确性：为什么代码永远可能有错

2026 年 8 月，一条新闻在程序员社区刷了屏：有人在高德纳（Donald Knuth）的传世经典《计算机程序设计艺术》（TAOCP）第二卷的长除法算法里，发现了一个藏了几十年的 bug。连"计算机科学之父"亲手写下、又被无数人反复阅读过的代码都会出错——这件事本身就是软件工程最深刻的一课。

为什么程序一定有 bug？

程序的本质，是用有限的代码去描述无限多种输入下的行为。一个函数哪怕只有几个整数参数，可能的输入组合也是天文数字——你不可能把每一种都跑一遍。测试只能证明"有 bug"，永远无法证明"没 bug"：测过的路径越多，只能说明剩下的盲区越少，而不是归零。这正是高德纳长除法 bug 能潜伏几十年的原因：它只在某些极其特殊的输入组合下才会触发，恰好落进了所有人测试的盲区。

图1：测试只能找反例，形式化证明才能覆盖全部输入

形式化验证：把程序当成定理来证明

有没有办法真正"证明"一段代码对所有输入都正确？有——形式化验证（formal verification）。思路是：把程序写成"定理"，把需求写成"要证明的命题"，然后用证明助手（如 Lean、Coq）一步步推导，由机器核对每一步是否正确。证明一旦通过，就等价于"这段代码在数学意义上绝对正确"——不是"测了很多次没出错"，而是"逻辑上不可能出错"。

图2：经典算法的 bug 往往只藏在极少数输入组合里

核心要点

• 测试 ≠ 证明：测试只能找反例，无法穷尽所有输入。
• bug 偏爱边界：特殊输入组合是 bug 的藏身处，高德纳的长除法就是例子。
• 形式化验证：用 Lean/Coq 把程序当定理证明，证明通过即"逻辑上不可能错"。
• 现实取舍：形式化代价高，关键系统（航空航天、金融、编译器）才值得全量证明；普通代码靠测试 + 边界审查兜底。