豐衛兵的標題“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.”
豐衛兵想從偽命題出發，“推出”其它偽命題為豐田開脫。其心可誅。特正視聽。
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.”
豐衛兵想從偽命題出發，“推出”其它偽命題為豐田開脫。其心可誅。特正視聽。
選擇“Disable on www.wenxuecity.com”
選擇“don't run on pages on this domain”
