国产编程语言，抓住了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，扫描下方二维码即可预约：