程式驗證的不可判定性（undecidability of program verification）

程式設計師夢想有一個工具，讀入你的程式碼與「它該做什麼」的規格，然後確認「是，這個程式符合規格」或「否，這裡出錯了」——每一次，全自動。Rice 定理與停機問題合起來證明：對於非平凡的行為規格，這樣一個完全通用的工具不可能存在。檢查任意程式碼是否滿足其行為的任意非平凡性質，是不可判定的。擋住停機檢查器的那道牆，也擋住了驗證器。

為什麼會這樣？一個行為規格恰恰就是程式所實作之「語言」（輸入—輸出行為）的一個性質。「這個函數對每個輸入都回傳已排序的串列嗎？」「這個程式永遠不會當掉嗎？」「它總會最終回應嗎？」——每一個都是非平凡的語意性質，而 Rice 定理說：對任意程式判定其中任何一個都是不可能的。即使是聽起來最簡單的規格，「這個程式會產生任何輸出嗎」或「它到底會接受任何輸入嗎」，也歸約到 A_TM，並繼承其不可判定性。

然而驗證卻是一個蓬勃發展的領域，這看似矛盾，直到你看見那些脫身之道。我們靠「限制問題」或「接受部分答案」來驗證：模型檢驗作用於有限狀態系統，其上的性質「是」可判定的；型別系統證明一類固定且可判定的性質；定理證明器在人類引導下驗證特定程式，而非全自動；健全的分析器則回報「已驗證」「確定有錯」或「無法判定」。這些都不牴觸定理，因為沒有一個聲稱自己是「對所有程式與所有規格的全自動判定器」。這個不可能性形塑了工程：我們以通用性換取可判定性。