科学“证明”的本质与软件开发

这是一个非常“深刻”和重要的结果。它说的是有一些数学陈述，我们永远无法在包含它们的逻辑系统中证明它们的正误。有趣和偶然的是这一理论本身是可以证明的！

因此我们已经有理由相信，某些知识对我们是不可访问的。

但是GÖDel并不是唯一持有这种观点的人。我们至少知道其它两个领域，在其中我们永远无法得到某些问题的答案。

进入计算机科学家

第一个领域的代表是计算机科学中的“停机问题”。Wikipedia是这样描述该问题的：

给出一个程序的描述和它的初始输入，决定程序在该输入下运行时会不会停止（完成）。另一种可能是程序将一直运行下去无法停止。

Alan Turing在1936年证明了对所有可能输入解决停机问题的通用算法是不存在的。我们说停机问题在图灵机上是不可判定的。因此，又有一类问题我们认为是没有可能的解决方案或答案的。

第二类问题来自组合数学界。²最常见的例子是著名的“旅行商问题”，这个问题乍一看几乎是平淡乏味的：

已知一些城市以及从一座城市到另一座城市的旅行费用，最便宜的遍历所有城市并回到出发城市的路线是什么？

对较少的城市这个问题就是困难的，而且随着城市数量的增加问题的复杂性迅速增长。实际上，当城市数量超过一个非常小的值时，即使使用计算机也无法解决这个问题了，因为需要计算的可能组合的数量增长得太快。³这个问题就是很多“NP完全”问题中的一个。⁴现在，对这类问题我们的最好解决办法是找出近似解。按照目前的知识，NP完全问题没有精确解。

关键在于，我们有若干来自数学和计算机科学的指示，告诉我们有一些问题是无法解决的，有一些假设是无法被证明正确或是错误的。但是这是一个悲剧吗？从我个人来说，我接受人类永远无法知道一切的观点。也许我们可以近似比我们可以证明的更多的东西。最终事情的某些方面可能被发现是不可知的。那么就由它们去吧。

对现实软件世界的启示

软件开发界中有两个领域直接与“知识的局限性”和“什么组成了一个证明”的提法相对应。前者是测试在软件开发中的作用，后者是迭代开发的提法本身。