01

前言

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

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

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

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

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

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

02

什么是形式化驗證？

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

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

    return None

很不幸，你手滑了，把 i

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

(1) 調(diào)用方傳進(jìn)來的是一個從小到大排好序的有序數(shù)組

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

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

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

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

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

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

1.前置條件

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

2.后置條件

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

3.不變量

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

它們就像定義一個合約，相當(dāng)于代碼的“法律條款”，需要用嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)方式定義出來（一會兒就看到）。

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

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

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

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

高下立判。

03

如何在MoonBit做形式化驗證？

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

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

proof_require 就是前置條件；

proof_ensure 是后置條件；

proof_invariant 是不變量；

其他的像：

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

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

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

}

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

}

sorted的意思是：對于所有的下標(biāo)i和j , 如果它們在數(shù)組的索引范圍內(nèi)，并且i<=j , 那么它們對應(yīng)的數(shù)組元素xs[i] <= xs[j] 。

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

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

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

04

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

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

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

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

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

開發(fā)者給出函數(shù)實現(xiàn)和合約意圖，AI 生成候選不變量和中間斷言，再由定理證明器進(jìn)行嚴(yán)格的機器檢驗。

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

證明器要么確認(rèn)每一步推理都成立，要么明確指出哪個目標(biāo)無法證明，AI 再據(jù)此修正并繼續(xù)嘗試。最終交付的，始終是經(jīng)過數(shù)學(xué)驗證的結(jié)果，從而避免“AI 幻覺”蒙混過關(guān)。

05

別的語言沒這么干過嗎？

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

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

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

還有一類是專為形式化驗證設(shè)計的語言，如微軟的 Dafny、Rocq（原 Coq）、Lean 等，它們雖然驗證能力更強，語言和證明系統(tǒng)天然一體。但它們?nèi)狈ψ鳛橥ㄓ镁幊陶Z言的生態(tài)基礎(chǔ)——沒有成熟的包管理、沒有廣泛的第三方庫、沒有大規(guī)模的工業(yè)用戶群。

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

06

總結(jié)

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

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

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

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

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