把定理兌現
到目前為止，這一階都活在「一本可讀、可擦、可重寫的無盡筆記本」的世界裡——圖靈機。但根據 邱奇-圖靈論題（Church-Turing thesis），那本筆記本恰好捕捉了任何真實程式語言所能計算的一切：Python、C、Rust、你最愛的試算表巨集，全都算在內。所以一條關於圖靈機被證明的極限，並非象牙塔裡的奇談。它是關於你實際寫出的軟體的鐵一般事實。當我們說某個問題是不可判定的，我們是永遠地這麼說——沒有任何未來的語言、更快的 CPU、更聰明的工程師，能交付一支對每一個輸入都正確求解它的程式。
把「不可判定」是什麼、不是什麼說清楚很值得，因為這個詞太常被濫用。不可判定不等於慢，也不等於只是像 NP 完全 問題那樣難。一個 NP 完全問題，比如 3-SAT，就我們所知是昂貴的——但它完完全全可判定：一支暴力程式總會以正確的「是」或「不是」停機，只是可能要跑上老半天。停機問題卻在另一個宇宙。沒有任何程式（無論多慢）能總是以正確答案停機——不是因為我們還沒找到它，而是因為你走過的那個對角線論證顯示：任何候選都會被迫與自己唱反調。不可判定是一堵牆，不是一座山丘。
三件你永遠做不完的工具
從開啟這一階的那個夢想說起：一個一般的停機檢查器——餵給它任何程式加上任何輸入，它就告訴你「這會終止」或「這會永遠繞圈」。那正是穿上工程外衣的停機問題，也正是那個對角線論證所殺死的東西。所以不存在一般的停機檢查器。注意「一般」這個小心的字眼：我們待會就會看到，一個只對某些程式有效的檢查器完全可能，而且每天都在出貨。不可能的是一個對每一個程式都永遠正確的檢查器——包括同事正是為了騙過它而寫的那個對手程式（第三篇裡那台自我指涉的「做相反的事」機器）。
接著是等價檢查器：給定兩支程式，判定它們是否計算出完全相同的函式——對每一個輸入都有相同的輸出。這是重構與編譯器最佳化的聖杯：證明我重寫的版本與原版行為一模一樣。它在一般情況下同樣不可能。程式等價是不可判定的，你能用一行歸約感受到原因：如果你能檢查等價，你就能問「程式 P 是否等價於那支對一切輸入都永遠繞圈的程式？」——而回答這個就會告訴你 P 究竟會不會停機，於是解了停機問題。一個歸約是把一個問題翻成另一個問題的翻譯器；這裡它把「停機」翻成「等價」，所以等價繼承了停機的不可能性。
最後是工程師感受最切身的那一個：一個完美的找蟲工具——一個能對任何程式判定它是否曾崩潰、漏記憶體、解參考空指標，或違反任何給定語意規格的工具。這每一項都是關於「程式計算出什麼」的非平凡性質，而那恰恰是萊斯定理（Rice's theorem）的地盤：一支程式所辨識的語言的每一個非平凡性質都是不可判定的。「對任何輸入都不崩潰」、「總是回傳排好序的串列」、「不含這類安全漏洞」——全是非平凡的行為性質，因此在完全一般的情況下全都不可判定。不存在任何分析器能對任何有意思的行為性質，同時做到健全（從不漏掉真正的蟲）、完備（從不誤報）、又全函式（總會停機）。
萊斯定理留下的逃生口
如果這一切聽起來像絕望，請用工程師的眼睛重讀萊斯定理，因為它遠比那份恐慌所暗示的狹窄。它的兩個逃生口，恰恰就是真實工具棲身之處。第一，萊斯談的是程式所辨識之語言的性質——它*計算出什麼*，而不是程式碼*怎麼寫*。純粹語法的問題大門敞開：「這份原始碼是否含有對 gets() 的呼叫？」、「這個迴圈是否有編譯器看得見的常數界限？」、「這個變數是否沿每條路徑都在使用前已被賦值？」——全都可判定，全都被你的 linter 與編譯器在毫秒內回答，因為它們檢查的是文字，而非最終行為。
第二個逃生口，正是支撐所有出過貨的型別檢查器與驗證器的那一個：放掉「健全、完備、全函式」三項要求中的一項，你就逃出了定理。真實工具會刻意選擇要犧牲哪一項，而每一種選擇都有一個你用這些工具時早已熟悉的名字。
- 放棄完備性（容許誤報）。靜態型別檢查器會拒絕某些其實本來能順利執行的程式，要求你證明自己的意圖。它總會停機、也從不放過真正的型別錯誤，但它保守——它標記為「無法到達的程式碼」也許真的無法到達。這就是型別系統、借用檢查器（borrow checker）與多數靜態分析器背後的取捨。
- 放棄健全性（容許漏掉）。一個啟發式 linter 或 fuzzer 能又快又多地找到真正的蟲，而且總會終止，但它可能悄悄漏掉一些。這類工具報「零警告」令人安心，卻永遠不是正確性的證明。這就是多數找蟲工具與測試套件背後的取捨。
- 放棄全函式性（容許不終止，或設逾時）。一個完整的程式驗證器或模型檢查器，在它跑完的案例上可以既健全又完備——但它可能永遠跑下去，或撞上逾時而回答「不知道」。這就是重量級驗證、以 SMT 為後盾的證明器，以及窮舉式模型檢查背後的取捨。
- 或者縮小定義域。一旦你限制在沒有無界迴圈的子語言裡——有限狀態協定、直線型程式碼、全函式片段——驗證就變得完全可判定。你並沒有推翻定理；你是走出了它適用的那個圖靈完備（Turing-complete）的場域。
不可能性如何在你用過的程式碼裡上演
一旦你知道往哪裡看，這些牆在日常工具上到處留下指紋。你 IDE 的「無法到達的程式碼」警告必然是近似的：判定真正的無法到達需要知道某個條件是否曾為真，而那不可判定，所以 IDE 在設計上不是過度警告就是警告不足。一個編譯器說「無法證明這個迴圈會終止」而拒絕內聯或向量化它，並不是膽小；它撞上了一堵牆並選了安全的那一邊。那令人頭痛、有時還報錯的「這個運算式恆為真／假」，是同一種近似。這些都不是工具的臭蟲——它們是停機問題無可避免的影子。
def confuse(P):
if halts(P, P): # SUPPOSE a perfect halt-checker existed
while True: # if P halts on itself, loop forever
pass
else:
return # if P loops on itself, halt
confuse(confuse) # ask the question about ITSELF
# halts(confuse, confuse) == True -> confuse(confuse) loops -> it did NOT halt. contradiction.
# halts(confuse, confuse) == False -> confuse(confuse) halts -> it DID halt. contradiction.
# Either answer makes halts() wrong. So halts() cannot exist.值得把為何這個矛盾滴水不漏釘死，因為這是整個這一階的承重觀念。機器 confuse 被允許對它自己呼叫那台假想的停機檢查器——一支程式可以把自己的程式碼當輸入，就像 confuse(confuse) 所做的那樣。無論檢查器對那個自我應用預測什麼，confuse 都被接線成去做相反的事，所以無論預測倒向哪一邊都是錯的。我們假設檢查器永遠正確；卻推導出它有時錯；因此假設為假。這就是反證法，你在數學工具那一階遇過的同一根槓桿，如今扳倒了你所能夢想最好用的那件除錯工具。
那為什麼這一切還行得通？
這裡有份安慰，而且它是誠實的、不是含糊帶過的。不可判定性說的是沒有工具對每一個程式都正確；它對你的程式什麼也沒說。證明裡那台對手機器是一個刻意扭曲、自我指涉的搗蛋鬼。你和你團隊實際寫的程式碼，絕大多數並不想擊敗分析器——它有界限看得見的迴圈、引數會縮小的遞迴，以及工具能啃得動的結構。型別檢查器、構造上即保證終止的語言、以及驗證器，能在那廣大而乖巧的多數上成功，正是因為真實軟體聚集的地方，離不可能性證明不得不伸手進去的那個病態角落很遠。
於是專業的姿態，正映照你早已用來對付 NP 困難問題的方式：你不要求一個完美的一般求解器，而接受一個有原則的部分解。對不可判定性而言，那意味著：近似（健全或完備，別兩者都要）、限制（用一個讓問題變可判定的子語言，比如沒有迴圈的設定檔格式）、設界（加個逾時，把「不知道」當成頭等的答案）、或協助（讓人類提供工具推不出的迴圈不變式）。這每一項都是正當、廣為部署的工程回應。定理並不禁止進步；它只禁止一個特定的幻想——那個普世、永遠正確、永遠停機的神諭。
一路退到最後，看看你爬過的這座階梯。DFA 是一個只記得當前狀態的旋轉閘門；下推自動機加上了一疊你只能碰最上面的盤子；圖靈機加上了那本無界的筆記本，並隨之帶來了完整的計算能力——而恰恰在那一刻，不可判定性現身了。更強的能力買到了一般性，也在同一口氣裡買到了「無法完整分析那份一般性」的不可能。那不是我們工具或我們聰明才智的缺陷；它是計算本身的一條結構性法則。精確知道那堵牆立在哪裡，正是把一位浪費整季去追求完美 linter 的工程師，與一位交付一個夠好的健全工具然後繼續前進的工程師區分開來的東西。