很多程序员自嘲「数学不好」。反过来看就是在憧憬基于数学理论写就的程序一定完全正确。其实并非如此。比如说，简单的 parser 可以严格基于有限态自动机和 LL(n) 理论，但写过的人都知道调试起来并不简单，即便充分测试也不能达到 100% 正确。
另一个例子是 3D renderer。无论是物理真实的 ray tracing 还是简单的 phong model，renderer 就是数学公式的代码实现。最近用 Metal by Example 的例子作为起点写程序。一开始还运行得不错。直到加上摄像位置的变换之后，near/far 平面会切掉在 view volume 里的模型。一开始也没在意，给 near/far 参数随便加上个余量凑合用。混了两个星期后偶然想到 Metal by Example 用的 projection 和 OpenGL 的一模一样，而 Metal 的 depth 范围不同于 OpenGL [1] 。在 Twitter 上向作者确认之后果然是这个问题。Metal by Example 经过了 15 个月的开发，出版也有一年左右。但是这个基本问题一直没有被发现。
软件开发的现状略带讽刺 —— 严格依据数学理论的程序反而缺乏有效的工具来验证其正确性。但这里其实也没什么讽刺性，因为数学本身的理论正确性也并非自动获得。一个新证明的正确性必需要经过其他数学家的人工验证，有时需要历时几年，甚至在最后才发现证明中的错误。数学的正确性是依靠数学界的「社交活动」达成的 [2] 。正如测试是软件开发的「社交活动」。
那么，数学理论是不是对软件质量没有帮助呢？也对也不对。数学理论并不能直接保证正确性，无法帮助发现错误。但是一旦发现了错误，数学理论可以帮助更快的修复软件。当我们在一个复杂的 ad hoc if-else 分支群里发现错误行为之后，很难立刻理清修复方案。而面对上文的 projection 错误，立刻就可以修正错误的参数。我把这种特性称为「可修复性」。可修复性和「正确性」不是一个层面的问题。其实软件开发的很多 best pratice 并非追求「正确性」，而是去提高「可修复性」。例如提高代码的可读性，以及我以前讨论的 MVC 模式的局限和突破，都是追求「可修复性」。经常听到很多团队讨论开发流程和实践的时候以「正确性」作为争论的立脚点，讨论怎么做才能节约测试成本，这样就走偏了。
「可修复性」不是「正确性」。也没有办法直接降低测试成本。但是「可修复性」是软件的一个隐形 spec。当错误被发现的时候，「可修复性」将一切争论局限在实现层面，避免了在设计层面的争论，更不会出现 feature vs. bug 的可笑争吵。「可修复性」还避免了修改中无意引入新的 bug。就目前的软件开发现状，我认为没有任何编程行为能有效提高「正确性」，那些能产生正确代码的程序员也无非是把代码丢给测试团队之前，自己先系统测试一番。一切编程本身的实践，都应该围绕「可修复性」来讨论。一切针对「正确性」的讨论，都应该交给测试领域。
脚注：
- Metal 的 canonical view volume 是 2x2x1，它的 z-buffer 范围不超过 [0, 1] 。OpenGL 为 2x2x2 ，z-buffer 范围为 [-1, 1] 。
- 当然，类似 Coq 这样的形式验证工具说明有可能改变这样的现状，但是距离实现仍然有一定距离。
技术奇异点 
发表评论