程式語言的形式化驗證領域不斷發展，像 coq-of-rust 這樣的工具旨在數學證明 Rust 應用程式程式碼的正確性。然而，社群討論揭示了關於形式化驗證能夠和不能夠保證什麼的重要細微差別，同時驗證生態系統中發生了一項重要的名稱變更。
形式化驗證宣告的現實
雖然 coq-of-rust 承諾透過數學證明使應用程式沒有錯誤，但開發者社群強調了一個重要區別。形式化驗證證明程式碼正確實現了規範，但不能保證規範本身沒有缺陷。
「我喜歡形式化驗證。但我認為這是對其提供功能的誤解。它讓你可以數學證明你的程式碼正確實現了規範。它不能證明你的規範沒有錯誤和漏洞。它不能證明你的規範正確實現了你的業務規則。」
驗證（程式碼是否符合規範？）和確認（規範是否符合實際需求？）之間的這種區別代表了質量保證中的一個基本概念。形式化驗證擅長證明不變數對所有可能的輸入都成立，這在規範比實現簡單的情況下特別有價值，例如在資料庫和檔案系統中。
Coq 更名為 Rocq：一項重要的改名
評論中提到的一個值得注意的發展是，coq-of-rust 的基礎——Coq 證明助手已更名為 Rocq。根據社群討論，這一變更源於一項社群調查，約 24% 的使用者表示對原名感到不適，認為在專業環境中使用它會感到尷尬或不自在。該專案現在正式名為 Rocq，可以在 rocq-prover.org 找到。
這次更名引發了不同反應，有些人認為這是必要的專業演變，而其他人則惋惜失去了他們認為無害的文字遊戲。
Rust 在驗證中的獨特地位
Rust 的可變-或-別名記憶體模型使其相比許多其他語言更適合形式化驗證。在這種模型中，資料要麼是可變的，要麼有多個引用，但不能同時具備兩種特性，這創造了一個驗證工具可以更有效構建的基礎。
社群成員指出，沒有這樣的模型，驗證就會變得和現有語言的所有驗證器一樣困難——在實際中同樣難以處理。這使得像 coq-of-rust、Verus 等基於 Rust 的驗證工具在驗證領域具有潛在優勢。
Rust 形式驗證工具評論中提及的
- coq-of-rust：將 Rust 轉換為 Coq 進行形式驗證
- Verus：旨在進行完整系統驗證（驗證檔案系統、Kubernetes 控制器）
- Creusot：從 MIR 轉換到 Why3（然後到 SMT 求解器）
- Ironclad/Gloire：不特定於 Rust，但是用 SPARK/Ada 編寫的經過形式驗證的作業系統核心
關於形式驗證的要點
- 證明程式碼正確實現了規範
- 不證明規範本身是正確的
- 當規範比實現更簡單時特別有用
- 受益於 Rust 的"可變-或-別名"記憶體模型
替代方法和競爭對手
形式化驗證領域不僅限於 coq-of-rust。社群成員強調了幾種替代方案，包括用於系統驗證的 Verus（用於驗證檔案系統和 Kubernetes 控制器），以及使用 SPARK 和 Ada 構建的 Ironclad 核心和 Gloire OS。
一些開發者表示有興趣看到類似的驗證方法應用於其他語言，如 Zig，特別是透過 Zig AIR 等工具，這表明整個系統程式設計生態系統對形式化驗證有需求。
對數學證明程式碼正確性的追求繼續吸引著各程式設計社群的興趣，儘管對形式化驗證實際能提供什麼有了更加微妙的理解。隨著工具的成熟和方法的多樣化，理論完美與實際實現之間的差距逐漸縮小，即使 100% 無錯誤程式碼的難以捉摸的目標仍然更多是願望而非現實。