为设么丰卫兵说的“All software bugs can be fixed"是个伪命题。

丰卫兵的标题“All software bugs can be fixed"是个伪命题。

1。在“fix”之前，你先得知道哪里有bug，bug是什么。或者说，你定下你对一个程序的specifications，我写一个程序交给你，你要看这个程序能不能满足你的specifications，如果不能，那就有bug。既然你要做判断，就必须是数学上严格的判断。从Godel和Turing的理论可以推出：总存在很多程序，无法从数学上严格地判断它们到底会做些什么，包括存在不存在bug。

2。什么叫程序／软件，要用Turing machine来定义。简单地说，就是平时我们运行地那些，但是它们用的内存大小没有上限。注意，它们在任何时候用的内存量都是有限的，但是要多少有多少。其实这在今天的网络上用distributed computing已经近似地可能了，可以用到整个网络地所有内存。再往上去，理论的不可能和实践的不可能就没有区别了，不过我们还是看理论说些什么。

3。什么叫严格地判断？就是给出数学上地证明，说某个程序是对或错。数学的证明要用到一定的公理系统和逻辑推理法则。比如欧几里得几何就是建筑在五大公理之上，你也许曾读过关于第五条，平行公理的几千年的争论和研究。曾有许多人试图用其它四条公理证明这第五条，都失败了。其实这是不可能的，如果否认平行公里，也能得到一套自恰的非欧几何。目前数学界在数学基础方面用的公里体系是ZFC的集合论，Peano的自然数公理，和2nd－order逻辑推理体系。

4。Godel证明了：给定任何公理体系，不管多么地复杂，包含多么多条公理，只要这些公理是互洽的（不是互相矛盾），那么一定存在有关自然数的真命题（就是说，是对的命题），它们是证明不了的。这适用于目前的数学体系，也同样适用于任何对它的扩充。你即使把证明不了的命题加为新公理，仍旧有证明不了的东西，而且永远是无限多的。

5。很难证明的命题很多。费儿马大定理就是有关自然数的一个命题，十几年前才被Princeton的Wiles证明。哥德巴赫猜想，还有孪生素数猜想等等，都是还没被证明的有关自然数的命题。最难的恐怕是黎曼猜想了，要用到复变函数，现在有许多数学家在研究，估计75％是先证明他的，20％左右觉得它不对，想找反例，还有5％左右正是觉得它可能是一个证明不了的命题。

6。每一个有关自然数的命题都可以用一个程序去一个数一个数地验证。（作为练习，编个程序验证费儿马大定理，看有没有反例）。只要假设内存可以要多少有多少，那么理论上就是Turing machine，每个数都能验证到。对于这个命题，如果程序找到一个反例，那就以错误结束，成为一个bug，要么crash电脑，要么造成丰田车加速，随你怎样。如果还没有找到反例，那就正常地继续找，也继续正常地让你开丰田车，直至永远。

7。如果你能严谨地判断这样一个程序不会有错，那么你就证明了它对应的命题是对的。因此，应用Godel的结果就是：一定存在有关自然数的命题，它是证明不了的，用来核实它的程序也就是判断不了对错的。这样的程序是无限地存在的。

因此，“All software bugs can be fixed"是个伪命题。

下面说说为什么指出你的伪命题那么重要。原因是，从伪命题出发，公里系统就不是自洽的了，数学家证明了：不是自洽的系统可以把任何假命题“证明”成真的。这是另一个数学大家Russell证明的。据说有人不信，挑战他说：“Assume that 1=2, prove that I am the Pope.”结果Russell不假思索就回答了：“You and the Pope are two, therefore you and the Pope are one.”

丰卫兵想从伪命题出发，“推出”其它伪命题为丰田开脱。其心可诛。特正视听。

所有跟帖： 

• 太复杂了，看了第二条就脑袋涨，提问：费马大定理和车有啥关系 -用户名被占用了- ♂ (0 bytes) () 02/28/2010 postreply 16:17:04

• 费被用来类比，说明丰卫兵用来替丰田开脱的前提就站不住脚 -UberAlles- ♂ (55 bytes) () 02/28/2010 postreply 16:54:53

• 请为我们这些普通劳动者考虑考虑，用通俗易懂的语言:-D -用户名被占用了- ♂ (0 bytes) () 02/28/2010 postreply 16:56:13

• 我最初对丰卫兵的回复就是通俗易懂，言简意赅. -UberAlles- ♂ (202 bytes) () 02/28/2010 postreply 17:24:33

• 你知道計算機用的是什么數學吗？ -tsc12- ♂ (52 bytes) () 02/28/2010 postreply 16:26:43

• 一個程式他會做四則咚悖?阏J為他不可能完全沒有bug嗎？ -UberAlles- ♂ (32 bytes) () 02/28/2010 postreply 16:43:28

• 虽然给你置顶，但还是要批评一句：论证太复杂 -biglow- ♂ (175 bytes) () 02/28/2010 postreply 16:42:46

• 请撤除置顶，没有车的内容。 -UberAlles- ♂ (201 bytes) () 02/28/2010 postreply 16:52:02

• 挺好的帖，置顶好。其实toyota也是很郁闷的，他们无法重复故障。 -企鹅肥肥- ♂ (286 bytes) () 03/03/2010 postreply 01:55:14

• 从软件工程的角度：Verification vs Validation -蜂油精- ♀ (605 bytes) () 02/28/2010 postreply 16:56:08

• 你最後一點，我問過，沒人回答 -tsc12- ♂ (50 bytes) () 02/28/2010 postreply 17:33:38

• 谁说有车厂能例外？不要问无意义的问题。 -UberAlles- ♂ (294 bytes) () 02/28/2010 postreply 17:47:19

• 那你推荐購買別的車廠的車就是偽命題 -tsc12- ♂ (38 bytes) () 02/28/2010 postreply 17:54:06

• 我推荐向来是基于“驾驶乐趣”，此地有目共睹。 -UberAlles- ♂ (49 bytes) () 02/28/2010 postreply 18:00:22

• 你這邏輯又是一個偽命題 -tsc12- ♂ (91 bytes) () 02/28/2010 postreply 18:20:14

• 嘿嘿，你还真不会阅读，给你个陷阱就钻。 -UberAlles- ♂ (198 bytes) () 02/28/2010 postreply 18:31:47

• 你貼的內容與標題不同，我說的是你內容邏輯錯誤 -tsc12- ♂ (0 bytes) () 02/28/2010 postreply 18:56:03

• 给人介绍女朋友，我说某甲有精神分裂，某乙更好。你说谁都有可能 -UberAlles- ♂ (62 bytes) () 02/28/2010 postreply 18:06:40

• 没人回答你那是不屑，你还自以为有理了？ -UberAlles- ♂ (98 bytes) () 02/28/2010 postreply 17:50:20

• 你對這個理論的了解根本是錯的 -tsc12- ♂ (0 bytes) () 02/28/2010 postreply 17:56:18

• 哟，请问你又是学什么专业的？ -UberAlles- ♂ (0 bytes) () 02/28/2010 postreply 18:01:27

• 而且，你还是弄错了，逻辑思维差了点。 -UberAlles- ♂ (300 bytes) () 02/28/2010 postreply 17:57:47

• 我的邏輯沒有錯 -tsc12- ♂ (167 bytes) () 02/28/2010 postreply 18:52:44

• “Bug必須有人先發現”只是你自己自以为是的定义。 -UberAlles- ♂ (0 bytes) () 02/28/2010 postreply 19:51:50

• 這是基本邏輯 -tsc12- ♂ (61 bytes) () 02/28/2010 postreply 20:38:45

• 小时候大人总是警告我们 -蜂油精- ♀ (60 bytes) () 02/28/2010 postreply 19:18:56

• 你沒這個水平，倒是有自知之明 -tsc12- ♂ (0 bytes) () 02/28/2010 postreply 19:31:25

• 不必生气。我早就懒得说话了 ：） -internuts- ♂ (0 bytes) () 02/28/2010 postreply 19:32:05

• 不生气不生气，跟这种人一般见识干嘛呢！ -咱也马甲一把- ♂ (38 bytes) () 02/28/2010 postreply 19:49:28

• 你说的很有道理，不光在工程领域，金融交易用的软件也是如此。 -UberAlles- ♂ (136 bytes) () 02/28/2010 postreply 18:18:35

• 给一个具体的软件，你们看看会不会crash？ -UberAlles- ♂ (1254 bytes) () 02/28/2010 postreply 17:40:26

• 這問題不難證明，我想了一下就得出答案 -tsc12- ♂ (84 bytes) () 02/28/2010 postreply 18:14:02

• 没读第一行吗？ -UberAlles- ♂ (23 bytes) () 02/28/2010 postreply 18:23:01

• 沒有一部電腦整數可以無限增加的，你連這都不懂 -tsc12- ♂ (0 bytes) () 02/28/2010 postreply 18:45:34

• 你事先不知道任何电脑的升级上限，道理就这么简单。 -UberAlles- ♂ (214 bytes) () 02/28/2010 postreply 19:59:26

• 哪有人写个程序不知道在哪run啊？您是Java程序员吧？program once, debug everywhere -先想一想再说- ♂ (0 bytes) () 02/28/2010 postreply 20:19:08

• 我终于明白您的逻辑了，您觉得一个bug free的程序是放之四海而皆run的啊？ -先想一想再说- ♂ (34 bytes) () 02/28/2010 postreply 20:22:17

• 本来就是计算理论的东西，当然要放之四海皆准。 -UberAlles- ♂ (56 bytes) () 02/28/2010 postreply 20:37:25

• 软件都有特定运行平台，脱离运行平台探讨软件无异于无本之木，无源之水 -先想一想再说- ♂ (0 bytes) () 02/28/2010 postreply 20:39:39

• 我早就說過學數學的是在象牙塔裡看世界 -tsc12- ♂ (206 bytes) () 02/28/2010 postreply 20:51:43

• 你没有明白他的意思，太令人遗憾。可计算理论是计算机科学的基础 -企鹅肥肥- ♂ (16 bytes) () 03/03/2010 postreply 01:34:37

• 另外不管计算机如何升级，一个躺着的8比他所能处理的数大躺着的8那么多倍 -先想一想再说- ♂ (0 bytes) () 02/28/2010 postreply 20:31:32

• 绝大多数工控软件都只有有限的输入和输出，理论上有限大小的真值表（true table)就可以验证 -先想一想再说- ♂ (0 bytes) () 02/28/2010 postreply 20:08:35

• 你连什么叫Bugs都不懂，还长篇大论。 -DrunkerKickass- ♂ (0 bytes) () 02/28/2010 postreply 22:23:05

• 一看到你强调“自然数”就知道你是行家 -企鹅肥肥- ♂ (0 bytes) () 03/03/2010 postreply 01:57:02