最近「知乎」上有几个关于王垠的问题，由此得知他写的《我和 Google 的故事》。最近得知他又放弃了博士学位。虽然对他的作为不是完全赞同，但是感慨他才华出众而且有勇气做想做的事情。一个匿名用户在一个问题下给出了这样的答案：
王垠是做学术的，而且是 PLT 程序编程语言领域。所以在这个领域他批评 Google 有足够多的理由。毕竟四大语言 C++, Java, Python, 和 JavaScript 在语言设计上可以吐嘈点在普通程序员里已经很多，更不用说一个此领域的博士生。而其中说到 Python，JavaScript 的语法语义分析，这本就是其研究领域的强项。
王垠为什么看不起 Test Driven ? 这个要从他的研究背景和方向就很容易理解。他在读书时候写作业，老板的要求就远超过 Test Driven。程序不但要求从输入到输出是正确，还要求程序能倒推运行，即给出输出结果，能产生所有可能的输入。王垠做的，是逻辑编程的方向，目的是通过逻辑推导演算去保证程序的正确性。为此不难理解，为什么他对测试是那么不以为然 —— 用大量测试就能保证程序逻辑正确么？
我相信王垠在形式化方法方面的成就绝非限于 toy problem。当初看到 L4 内核的正确性被形式化证明的消息也很感兴趣。但之后发现此类方法需将源代码经过某种建模转换才能带入形式化符号系统。对于实际的产品，这种转换可能过于简化。感觉在软件开发中的实际作用有限。
不过最近有关 TDD 的思考让我有了一些新想法，似乎形式化方法的实际意义并非那么「有限」。至少，相对于很多人鼓吹的 TDD 方法的根基 —— Unit Test 这种特定类型的测试，形式化方法的局限性还那么突出吗？
复杂的软件系统中一个 class 的实例化 (instantiation) 和执行通常需要调用所依赖的其它 dependent class 的代码。Class 之间的 dependency 是 Unit Test 的最大障碍之一，因为 Unit Test 需要尽量避免触及被测 class 以外的代码，特别是运行速度较慢或附带影响较复杂的代码，例如需要访问数据库或文件系统。所以 Unit Test 需要名目繁多的 dependency breaking 技术 —— 避免调用 dependent class 代码的方法。常用的 dependency breaking 技术包括 interface/implementation extraction、mock object、parameterise constructor、static setter 等等。Interface/implementation extraction 方法为 Unit Test 特地增加产品代码的继承层次。Mock object 在增加的继承层次下构建虚假的 dependent class，令其功能从测试角度模拟真实的 dependent class，同时避免访问数据库等不利于 Unit Test 的因素。
这些所谓的「技术」让我非常不舒服。因为它们触及到测试存在本质原因 —— 人们无法保证代码的正确性。在测试前根据某些假定对代码肆意地修改，等于是在宣布：我认为自己可以无需测试即猜测这段代码的这部分是正确的，可以替换为一个 mock object 而无损对其它部分的验证。实际上，软件开发者（包括测试者）根本无法通过测试以外的手段证明软件的任何一部分是正确的。Dependency breaking 本身违背测试的根本原则。
在 Robert L. Glass 的《Facts and Fallacies of Software Engineering》里，有这样一个 Fact:
Fact 33
Even if 100 percent test coverage were possible, that is not a sufficient criterion for testing. … 40 percent (of software defect emerge) from the execution of a unique combination of logic paths. They will not be caught by 100 coverage.
注意 Robert 这里指的是包括系统测试在内的各种测试。那么，可以想像在充斥 mock object 的情况下，分离测试单个函数的功能的 Unit Test 能在多大程度上保持代码的正确性。
我相信有些人已经开始准备反驳 —— 不能因为 Unit Test 的效果不够完美就否定其存在的意义。它还是能相对提高代码的质量。那么，我觉得这些评价无疑承认 Unit Test 只是一个「聊胜于无」的技术。但不要忘记这个「聊胜于无」的技术是有成本的，如果它的投入产出效率不及其它替代技术，那么连「聊胜于无」这个称号也无法胜任。上一篇《关于单元测试》提过了 SCM 和 TDD 的投入产出效率比较。这次回到王垠的研究领域。如果我们认为形式化证明存在模型过于简化这样的局限性，不妨审视一下 TDD 所鼓吹的 dependency breaking，其本质无非也是一种建模简化技术。TDD 在建模简化之后仍然需要搭建一个基本环境实际运行幸免于修改的代码来验证其正确性。而形式化方法全过程都无需搭建运行环境。似乎后者的成本更低。
以我有限的理论基础，不能像之前 SCM 和 TDD 的比较那样，对形式化方法的效率下一个比较确定的结论，也许形式化方法目前还不够用于实际的软件产品开发。即便如此，我相信形式化方法比 TDD 更有前景。因为形式化方法的一切缺陷，Unit Test 在本质上都无法避免；另一方面，鼓吹 TDD 的人丝毫不以为自己在进行着过度简化，也不认为自己鼓吹的技术有其它更有效率或者更有前景的替代物。
技术奇异点 
2012/09/26 1:52 下午 |
You are what your program was also my maxim. Till I found that you are not what you program. People don’t choose a self, they live one.