通用停機檢查器的不可能性（impossibility of a general halt checker）

這裡把停機問題兌現成給程式設計師的實用忠告。不可能存在這樣一個工具：給定任何程式與輸入，它總能正確回報該程式會結束還是會掛住。不是現在不行，不是有更快的電腦就行，而是永遠不行——這是被數學排除的，不只是還沒被造出來。如果有人聲稱寫出了一個對所有程式碼都有效的完美通用無窮迴圈偵測器，那他錯了，就和有人聲稱造出永動機一樣錯。

這聽起來令人喪氣，但現實更微妙、也更有用。不可能性只針對「全函數且永遠正確」的檢查器。實務上，有用的近似檢查器存在且無所不在：一個工具可以對許多程式正確地證明會停機，對另外許多程式正確地證明不會停機，而對真正困難的剩餘部分誠實地放棄，說「我判斷不出來」。這種三結果設計——是、否、或不知道——繞過了定理，因為定理只禁止「必須永遠表態為是或否」的檢查器。編譯器、靜態分析器、停機證明器每天都正是這麼做。

更深的教訓是把你的期望編列正確。你可以對受限語言驗證停機（只有有界迴圈的語言顯然總會停機），對特定程式驗證停機（用手寫證明或一個排序函數），或用偏保守、寧可錯在安全一側的工具。你無法擁有的，是一個對一切可想像的程式碼都能解決停機、毫無錯誤答案也毫無棄權的按鈕式神諭。知道這點能讓你不去追逐一個不可能的產品，並指向那些可以達成的產品。