小編精選 - 技術文章翻譯 · 11月02日

我發布了讓 AI 撰寫證明、以安全方式進行開發的語言 Tauto！

前言

讓 AI 幫忙寫程式，已經變成理所當然了。
可是，你有沒有過這種悶悶不安的感覺？

AI 寫出來的程式，差異全部讀完已經到了極限
測試過了。可是 沒寫測試的情況也沒問題嗎？
就算問 AI「為什麼這樣是對的？」，也不知道它的說明是不是真的對

程式生成得越快，負責確認的人負擔就越大。

所以我正在做一個語言 Tauto，讓 AI 在寫程式的同時也寫出「這段程式一定滿足這個性質」的證明，而人類則負責審查那些性質（命題）。

安裝方法與執行方式可以參考儲存庫的 README 裡的 Quickstart（本文中的範例，已在文章公開時同步釋出的版本上確認可運作）。

本文會介紹：

有了證明之後，到底好在哪裡
測試和證明要怎麼分工
AI 時代的工程師，應該確認什麼

並透過具體例子來說明。

適合讀者

正在做 AI coding（vibe coding），卻對如何確認品質感到困擾的人
在寫權限、金流、狀態管理等，一出錯就很麻煩的程式的人
對「證明」或「型別」有興趣，但覺得太難而遲遲沒有入門的人

比如說，這種 Bug

假設部落格服務有一條規則：「只有文章作者可以刪除該篇文章」。

但是程式一大起來之後，就可能出現：

從畫面刪除時有檢查作者
但 從 API 刪除時漏掉檢查

這種 前後不一致的狀態。
結果就是，可以偷偷刪掉別人的文章。

這叫做「存取控制不足」，也是 OWASP Top 10 中名列前茅、Web 應用常見的弱點。

在 Tauto 裡，我們會把這條規則寫成命題，並且證明它對任何輸入都成立。

// 操作的人與文章之間的關係
pub(open) inductive enum Relation {
  Author
  Stranger
}

// 能不能刪除文章
pub fn can_delete(r: Relation): Bool {
  match r {
    Author => true
    Stranger => false
  }
}

// 命題：「如果能刪除，那麼那個人就是作者」
pub theorem delete_only_author(r: Relation, h: can_delete(r) = true): r = Author {
  match r: r = Author {
    Author => Refl
    Stranger => False::elim(false_ne_true(h))
  }
}

如果有人（或是 AI）把 Stranger => true 改掉，這個證明就無法通過，會直接編譯錯誤。

$ tauto check --lang ja post.taut
FAILED  delete_only_author: post.taut:19:17: 型別不一致：預期 `false = true`，但實際上是 `can_delete(Stranger) = true`
  差異部分：預期 `false`，但實際上是 `true`
2 ok, 1 failed, 0 incomplete; 0 skipped, 0 from imports; axioms: none

人類不必把證明的每個細節都追完，而是可以把重點放在審查 delete_only_author 的結論與前提是否符合規格。

這是個入門用的小例子（如果只有兩種情況，靠測試也能涵蓋）。證明真正派上用場的時候，是輸入與狀態的組合變多，讓完整測試變得很困難的時候。

另外，這裡證明的是針對 Relation 的判定規則。在實際應用中，伺服器端會去比對已登入使用者與文章作者，進而求出 Relation。接著，把刪除流程集中到一個函式上，並要求它以 can_delete(r) = true 的證明作為參數，那麼型別檢查就能阻止它在沒有證明的情況下被呼叫。至於從外部程式直接操作資料庫之類的路徑，則不在這個證明的範圍內。

Tauto 的特色

安全：命題中寫出的「不能做的事」，可以對所有輸入證明它不會發生
以 AI 撰寫為前提的設計：即使大量交給 AI 寫，證明內容仍由機器檢查，所以人類可以專心確認命題
容易閱讀的證明：在重寫等步驟中，會寫出當下要證明什麼（goal），人類與 AI 都看得懂
真的可以運作：可編譯成 Rust 與 JavaScript，也能透過 Rust 轉成 WebAssembly

測試與證明的分工

證明不是測試的替代品。 兩者擅長的事情不同。

測試證明可確認的範圍你寫到的輸入 針對所有輸入 擅長的事情實際執行並確認「真的會這樣」保證「絕對不會發生」適合的對象外部 API 整合、效能、UI、執行環境中的行為權限、狀態轉移、計算規則舉例來說，像下面這些事，光靠證明還不夠，在實際環境中做測試或量測 仍然很重要。

外部 API 或函式庫是否會如預期回應
在真實瀏覽器或伺服器上，速度與記憶體是否足夠
最根本的是，命題是否真的正確表達規格（實際拿具體輸入跑看看，往往能發現命題寫歪了）

反過來說，像「別人的文章 絕對不能 刪除」這種規則，一旦輸入或狀態組合變得非常多，光靠測試要完整涵蓋就很困難。這就是證明登場的地方。

用測試確認「會照預期運作」，用證明確認「指定的性質一定成立」。

Tauto 本身也是這樣做的：語言實作用數千筆測試案例確認，而型別檢查核心的部分性質則用 Lean 證明。

如何確認 AI 寫的程式

在 Tauto 裡，我們用以下方式表達正確性：

把性質寫成命題
再用程式寫出對應的證明

另外，透過 依賴型別 的機制，可以比一般靜態型別系統更進一步，用型別對更多事情加以約束。

只要編譯通過，就代表機器已經確認該命題成立。

因此，人類不必逐行讀完證明本文，而是可以把重點放在「命題怎麼立才對」。

但也有一些要注意的地方：

能保證的只有你在命題裡寫出的性質。如果命題本身偏離規格，那只是把偏掉的東西正確證明出來而已。
外部函式庫、編譯流程等，不在證明範圍內的部分，仍需要靠測試等其他方式確認。
這個保證依賴於檢查證明的編譯器本身（型別檢查核心）正確運作，以及證明中使用的公理與外部程式前提是正確的。因此，核心會盡量保持精簡，而 tauto check 也會列出用到的公理（上面的例子是 axioms: none）。

讓人類與 AI 都容易閱讀的證明

機器能檢查，不代表證明就可以不讀、或是不用寫得能讀。
閱讀證明時，有時也能發現命題或規格本身有問題。

因此在 Tauto 裡，只要使用重寫之類的步驟，就要求明確寫出該步驟前後的 goal。例如，「乘法交換律」的證明片段可以像這樣：

Succ(k) => by rewrite!(mul_succ_l(k, n)): nat!(`$n * $k + $n = ${Succ(k)} * $n`) {
  ⊢ nat!(`$n * $k + $n = $n + $k * $n`) from by rewrite!(mul_comm(n, k)) {
    ⊢ nat!(`$k * $n + $n = $n + $k * $n`) from add_comm(k * n, n)
  }
}

⊢ 後面的內容，就是「現在這一步要證明什麼」。
因為每次重寫都會把 goal 寫出來，所以證明可以從上往下順著讀。