為設麽豐衛兵說的“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