國產編程語言，抓住了AI的風口，這次真的領先了！

01

前言

這兩年，AI編程進化速度實在驚人，程序員只需要把需求說清楚，AI很快就能給出一版能跑的東西。

但能跑 ≠ 正確，頁面沒報錯，不等于認證、權限、狀態流轉、邊界條件沒有坑。于是程序員被迫花大量時間做代碼審查，成了“審核官”和“背鍋俠”。。

但人的注意力也是有限的，代碼少的時候，人還能兜底。代碼一多，邏輯一繞，程序員只能對著一大堆代碼哀嘆了，最終，review 從“認真審查”變成“差不多看過”。

那么問題來了：有沒有一種辦法，描述程序應滿足的約束，并自動檢查實現是否真正滿足這些約束呢？這樣一來，代碼的正確性就有很大的保證，不用程序員苦哈哈地去審查了。

這正是“形式化驗證”要解決的事，只是過去門檻太高，難以普及。

最近我注意到國產編程語言MoonBit發布的0.9版本中，引入了一個非常讓人振奮的決定：把形式化驗證加入到了日常開發流程當中！

02

什么是形式化驗證？

我們拿一個案例來看一下：二分查找算法。二分查找的概念非常簡單，就是每次折半嘛！

你很自信，迅速寫出一版，提交了：

    return None

很不幸，你手滑了，把 i

其實，普通程序員寫二分查找時，類似小細節很多，只是這些“隱含假設”都在腦子里：

(1) 調用方傳進來的是一個從小到大排好序的有序數組

(2) 每次判斷的區間范圍是[i,j)，搜索區間一直在縮小

(3) 對于每次循環，“中間點”左邊的元素一定 < key ，右邊的一定>key

(4) 返回值要么是None，要么是數組中某個元素的索引

但這些假設你平時不會寫出來，就是寫出來也是注釋或者文檔。

如果能把這些規則也寫出來，當成程序的一部分，可以對程序自動進行驗證，那豈不是能自動找到代碼寫錯的地方，代碼豈不是固若金湯了？

形式化驗證就是這么做的，它包括3個部分：

1.前置條件

例如：函數調用者必須保證，輸入的數組是從小到大排序的，否則就報錯。

2.后置條件

例如：我這個函數保證：要么返回None（不存在），要么返回一個索引值i，使得xs[i] = key。

3.不變量

例如：在每一輪循環中，j都小于數組的長度， i 左邊的所有元素都 < key, j 右邊的所有元素都 > key.....

它們就像定義一個合約，相當于代碼的“法律條款”，需要用嚴謹的數學方式定義出來（一會兒就看到）。

MoonBit拿到這個合約和代碼以后，會進行推理：初始狀態成立嗎？每一步都不破壞不變量嗎？結束時能推出結果嗎？

如果三步都成立，證明完成，你寫的代碼沒有問題，滿足合約。

值得注意的是，傳統的測試方式可能是驗證100組數據，只能說明這100組沒問題，這是抽樣驗證。 “我試過很多例子，看起來沒問題。”

而MoonBit是數學證明，對于任意的數組長度，任意的數據分布，任意的key，都成立。“我寫了一份證明，這段代碼在邏輯上不可能錯！”

高下立判。

03

如何在MoonBit做形式化驗證？

好，我們來看下MoonBit中如何表達這些前置條件，不變量，后置條件。

同樣的二分查找算法，在MoonBit中是這么寫的：

proof_require 就是前置條件；

proof_ensure 是后置條件；

proof_invariant 是不變量；

其他的像：

sorted,binary_search_ok,all_less_before,all_greater_from,binary_search_ok都是謂詞，也需要明確地定義出來：

它們看起來有些枯燥，但是實際上仔細看一下還是很容易理解的（學過離散數學的看到這些會更親切）。

例如這個in_bounds謂詞,它的意思是：下標 i 是合法的數組索引，滿足i>=0 , i

}

下面這個sorted謂詞中，出現了一個新符號?，意思是for all（對于所有）。? i 就是對于所有的i。

}

sorted的意思是：對于所有的下標i和j , 如果它們在數組的索引范圍內，并且i<=j , 那么它們對應的數組元素xs[i] <= xs[j] 。

翻譯成大白話：數組是有序的，是從小到大排列的。

再強調一遍，這些謂詞和“合約”它不是注釋，不是文檔，它們就是Moonbit代碼的一部分。

當開發者執行 moon prove 時，MoonBit 工具鏈會將程序邏輯和謂詞定義翻譯為約束求解問題，再交由 Z3 等 SMT 求解器進行自動化驗證，確保你寫的二分查找算法滿足其合約承諾。

04

不會寫合約怎么辦？讓AI來！

看到這些謂詞，可能大部分程序員都懵了：這玩意兒寫起來比那個二分算法都復雜，對程序員的要求太高了，我可寫不了。

確實，之前寫謂詞和不變量是一種專家技能，只在極少數對安全要求極高的場景（航空系統，操作系統內核，醫療設備等）中使用。

不過，MoonBit成功開辟了一條路：借助 AI 降低這一門檻。

事實上，前文中的二分查找——包括循環不變量、謂詞定義以及 proof_assert 引導鏈——大部分都由 AI Agent 輔助生成。

開發者給出函數實現和合約意圖，AI 生成候選不變量和中間斷言，再由定理證明器進行嚴格的機器檢驗。

這形成了一種精妙的協作模式：AI 負責“猜”，證明器負責“查”。AI 可能會出錯——它生成的不變量可能過弱，中間斷言也可能遺漏——但錯誤的猜測無法通過證明器的審查。

證明器要么確認每一步推理都成立，要么明確指出哪個目標無法證明，AI 再據此修正并繼續嘗試。最終交付的，始終是經過數學驗證的結果，從而避免“AI 幻覺”蒙混過關。

05

別的語言沒這么干過嗎？

形式化證明不是全新的概念，別的語言也干過，但是 MoonBit 首次開創性地將形式化驗證作為語言的一等特性，原生內置了。

例如C 語言的 Frama-C、Java 的 OpenJML、Rust 的 Creusot， 它們都是在現有語言上疊加了驗證能力，合約和語言是分離的，只能通過注釋或者宏注入，相當于語言不可見的外掛。

在這種情況下，IDE肯定就無法原生理解這些合約了，只能靠外掛插件來補全、跳轉。 當編程語言升級的時候，外掛的驗證工具通常需要滯后數月甚至數年才能跟上。

還有一類是專為形式化驗證設計的語言，如微軟的 Dafny、Rocq（原 Coq）、Lean 等，它們雖然驗證能力更強，語言和證明系統天然一體。但它們缺乏作為通用編程語言的生態基礎——沒有成熟的包管理、沒有廣泛的第三方庫、沒有大規模的工業用戶群。

MoonBit 的差異化在于垂直整合：合約、謂詞、循環不變量和 proof_assert 都是語言語法的一等成員，編譯器直接理解這些結構，IDE 可以像處理普通代碼一樣對驗證注解提供語法高亮、自動補全、類型檢查和錯誤定位；moon prove 作為構建系統的內置命令，與 moon build、moon test 并列。從編寫代碼到編寫證明，再到運行驗證，全部在同一套語言、同一個 IDE、同一條命令行中完成。

06

總結

一門語言想要世界流行，不僅自身實力要強悍到能真正解決一類問題，遇到風口也很重要，比如Java，遇到了互聯網大爆發的風口，趁著大型復雜網站缺乏有效編程語言成功上位，Ruby(RoR)遇到了快速開發Web2.0網站的風口，Python則遇到了科學計算和人工智能的東風......

作為國產編程語言，MoonBit正在努力抓住AI時代，作為ChatGPT之后出現的編程語言，它不但在設計上就考慮了和 Codeing Agent 深度整合，也充分利用AI輔助，工具鏈整合，開創性地將形式化驗證作為語言的一等特性，原生內置，將形式化驗證的門檻大大降低。

隨著MoonBit這套能力不斷完善，我相信“證明代碼正確”能夠像編寫測試和運行構建一樣，逐步成為軟件工程中的常規實踐。

AI時代的編程語言，我很看好MoonBit。

如果你想了解更多關于MoonBit形式化驗證的功能，感受下形式化證明帶來的威力，歡迎參加周六（4-25）在深圳舉辦的Meetup，掃描下方二維碼即可預約：