我在一天早上看到同事转来的一个标题“Lauren Tan 看好 Bend代码库可形式化验证自身代码审查问题即被解决”。说实话第一反应是先翻到评论区看有没有人骂。“代码库可形式化验证自身”这种说法实在有点唬人代码审查也不可能因为一门语言的出现“即被解决”。但那天下午我还是去把 Bend 的文档和示例翻了一遍越看越觉得这个标题虽然夸张指向的却是真问题代码审查的瓶颈确实很多时候不是人不努力而是语言没有给审查者提供足够的可验证性。先说清楚我理解这句话的语境。Lauren Tan 看好的不是某个能自动修 bug 的工具而是一种语言设计方向当代码库从诞生那一刻起关键约束就被内置到语言里代码审查里大量机械化的检查工作就被前置到了编译器和静态分析阶段。这篇文章想把我对 Bend 的理解、实际动手跑过的体验以及我对“代码审查被解决”这个判断的怀疑和认可都摊开聊聊。1. 一个看起来像营销口号却值得反复琢磨的判断1.1 标题里那句话我在意的是“验证自身”“代码库可形式化验证自身”这个表达很容易被理解成代码能自己证明自己没有 bug。如果真能这样那代码审查确实可以直接解散了。但稍微理性一想就知道任何程序都只能在给定规格下被验证而规格本身仍然来自人。Lauren Tan 真正想说的应该是代码库具备了一种能力把大量需要审查者凭空推理的内容变成语言层面可自动检查的规则。Bend 之所以被她拿出来说是因为这门语言的设计在“可验证性”上做了很多主流语言不愿意做的事。变量不可变函数没有副作用共享状态被语言直接禁止。这些约束在写代码的时候看起来像束缚但在审查的时候全都是红利。审查者面对一个不可变值的函数不需要在脑子里模拟“这个变量在某个分支里被改成什么值”因为变量根本不会被改。这种“验证自身”的底气不是运行时某个框架提供的而是语言层钦定的。我后来在 Bend 里写了几个简单例子第一感受就是编译期能查错的范围比想象中大很多因为语言把很多“运行时错误”直接变成了“不可能出现的结构”。1.2 代码审查的痛点本质是“人眼执行不了所有路径”做过程序员的人都懂代码审查最累的不是读代码本身而是模拟执行。一个稍微复杂点的函数可能涉及到初始化顺序、寄存器位操作、超时分支、错误恢复路径。你 review 时看的是文本但心里跑的是运行时行为。模拟个三五层还行再往下注意力就开始衰减边界条件和清理路径就成了重灾区。这也是为什么工程上会引入 lint、类型检查、单元测试、CI 静态分析。它们不是替代 review而是替 review 提前完成一部分机械验证。大多数团队其实已经在做这件事只是没有意识到这其实就是“形式化验证”的雏形类型检查证明了一部分不可能出现的运行状态单元测试验证了一部分特定输入下的输出静态分析扫描出了一部分潜在的未定义行为。Lauren Tan 的话说白了就是把这个趋势推到更底层与其靠一堆外部工具对代码库做事后验证不如让代码库从一开始就用一种更容易被验证的语言来写。审查者后续要做的就只是在已经验证过的地基上做判断而不是从零开始一步步推理所有可能路径。2. Bend 的底牌Python 语法、HVM2 和自动并行2.1 HVM2 到底在并行什么我第一次听说 Bend 时对它最出圈的宣传点是“像写 Python但能自动并行到 GPU 上”。当时第一反应是“又是编译器魔术”。后来查了 HigherOrderCO 团队的资料才发现底层的东西确实有点意思Bend 跑在一个叫 HVM2 的高阶虚拟机上计算模型来自 interaction net中文一般叫相互作用网。用生活类比来理解的话可以想象你有一堆牌每张牌上写了一条重写规则。只要两张牌的内容互不依赖就可以同时翻牌、同时重写、同时把结果传给下一堆牌。HVM2 做的就是把这堆牌尽可能均匀地分配到不同 CPU 核心或 GPU 线程上去。程序员不关心哪个核执行了哪一张牌只需要保证牌与牌之间没有隐藏的依赖。这带来一个很直接的工程红利不需要写线程不需要加锁不需要处理共享内存同步。在 Bend 里一段递归程序天然被拆成多个独立子计算HVM2 自动把它们扔到可用硬件资源上跑。我按照官方示例写了一个简单的递归求和用bend run跑的时候能明显感觉到计算资源被吃满而代码里没有任何并发原语。2.2 不可变变量写起来别扭查起来省心Bend 语法长得像 Python缩进、关键字、函数定义风格都很接近。但有一个本质区别Bend 没有变量重赋值。你写x x 1这种语句编译器大概率当场拒绝。几乎所有涉及状态变化的东西都要用递归、fold、bend 这类结构来重新表达。对从 C 或者 Python 转过来的人来说头几天非常难受。我一开始写着写着就下意识去改循环变量结果全是编译错误。但适应之后一个非常明显的好处出现了代码里少了一整类“状态被谁改了”的问题。不可变变量对并行是必须的因为没有共享状态就不会有竞态条件。对代码审查同样是巨大红利审查者不需要在脑子里维护一张“每个变量在不同路径上的值”的大表。函数输入确定输出就确定这种确定性本身就是可验证性的基础。你在 review 一个 Bend 函数时看到的就是一张清晰的数据流图而不是一团随风摇曳的状态。3. “形式化验证”为什么在 Bend 这里变得更现实3.1 可验证性的头号障碍共享状态和副作用形式化验证在工程界喊了很多年一直没有大规模落地。很多人以为难点在数学公式太抽象、工具太复杂但以我在实际项目里的观察真正的障碍是主流语言里的共享状态和副作用。一个函数如果能访问外部全局变量能改数组元素会抛出运行时异常那它每次执行的结果都可能不同。你要验证它的行为就必须考虑所有可能的外部状态组合。组合数量随着变量数量指数增长很快就超出人力范围也超出普通工具能处理的范围。比如 C 语言里的一个全局缓存可能被中断处理函数、主循环、线程同时访问你想证明某个操作不会读到脏数据难度不亚于做一道复杂的离散数学题。Bend 从语言层面把这类问题掐断了没有共享可变引用没有隐式全局状态函数纯度被强制约束。这相当于把一栋楼的全部承重墙提前画好剩下的房间再怎么装修都不会影响整体结构。验证代码行为这件事从“推理任意可能的执行历史”变成了“观察纯函数表达式的语义”后者的机械化程度高得多。3.2 语言层面的自我检查类型、纯函数和所有权Bend 的编译过程本身就内建了不少检查。类型不匹配在编译期就报错递归结构会被识别变量的不可变约束被强制。虽然没有成熟的定理证明器但语言本身给出的强保证已经相当于程序在编译阶段执行了一部分静态验证。我会把这种设计叫“语言内建的可验证性”。它不需要你额外学习 Coq、Lean 或 TLA只需要你在写代码时接受语言规则编译器就会自动帮你排除一大批潜在错误。比如在 C 里你要靠约定来保证“这个指针不被别处修改”违反约定的代码可能编译通过然后运行崩溃。在 Bend 里这种约定直接表现为编译器拒绝接受可变共享状态。用交通设计来类比如果一条路设计成单行道你就不需要在每个路口立“禁止逆行”的标志。Bend 的不可变和纯函数语义就是在设计上删掉了一大批“逆行”的可能性。审查者要检查的路口自然变少剩下的每个路口都更值得投入注意力。3.3 和真正的定理证明器相比Bend 还差得远这里必须泼一盆冷水Bend 距离“代码库可形式化验证自身”还差得很远。它没有依赖类型没有证明项没有自动不变量归纳。你想证明一个递归函数的结果永远非负或者证明一个循环必然终止Bend 并不会自动帮你做你仍然需要外部工具或人工证明。这意味着标题里的“即被解决”应该理解成“大大降低了解决门槛”而不是“完全解决”。Bend 做得好的是把“不可变”“无副作用”“无共享状态”这些有利于验证的特性变成了语言强制规则但它还没有提供完整的逻辑框架让人可以在语言内部写出“这个函数满足某某性质”的证明。所以我的判断是Bend 是一个非常适合做形式化验证实践的语言基础但它本身还不是一个成熟的验证工具。Lauren Tan 的乐观更多是在说“语言设计终于开始往可验证性倾斜了”而不是“验证问题已经被彻底解决”。4. 一个现实例子用 HAL 库驱动 OLED 时审查最容易漏什么4.1 一段常见的 OLED 驱动代码Review 到底看什么最近不少做嵌入式开发的朋友在搜“hal库驱动oled代码”我猜大家是在调 SSD1306 这类经典 OLED 屏。这种代码在开源社区里一抓一大把但真要把它放到代码审查桌上值得盯的点比想象中多I2C 或 SPI 总线初始化参数是否匹配从机地址拼接对不对命令字节和数据字节的选择是否按手册来显存数组大小和刷屏循环边界是否一致错误状态、超时分支有没有被吞掉。我拿一个简化版 I2C 刷显存例子来说明uint8_t oled_buffer[1024]; for (uint16_t i 0; i sizeof(oled_buffer); i) { HAL_I2C_Mem_Write(hi2c1, 0x78, i, 1, oled_buffer[i], 1, 100); }这段代码看起来没问题但 review 时你会犹豫0x78是不是忘了带上读写位i作为 OLED 显存地址范围和oled_buffer一致吗如果 OLED 有分页机制i从 127 跳到 128 时是不是正好跨页超时时间 100ms 够不够这些问题每一个都不难但全叠在一起人眼很容易漏掉其中一个。4.2 人眼 review 为什么总在边界处翻车我讲一个自己踩过的坑。有次 review 一段 OLED 刷显存逻辑某处用一个uint8_t当循环索引结果刷新到第 256 次时索引从 255 溢出回 0显存内容从第 256 字节开始全部写错位。那个 bug 在代码里待了整整一周直到整块屏幕出现条纹状花屏才被定位出来。事后看代码非常明显但人在 review 时很难盯着一个类型定义然后在脑子里走完 256 次循环。这种问题本质上属于“取值范围和边界条件验证”。靠人眼做成本高、容易腻靠测试做不一定覆盖得到靠静态分析工具做又需要额外配置和建模。如果语言本身支持表达“这个索引必须保持在 0 到 buffer_size-1 之间”并自动检查审查负担会小得多。这也是为什么我会把 HAL 驱动 OLED 代码和 Bend 放在一起想。表面上前者是嵌入式 C后者是 HVM 上的并行语言领域完全不搭。但它们背后的诉求一致代码审查最怕的就是“隐含边界”而隐含边界最好由语言来显式表达。4.3 如果驱动逻辑也能被机器证明一部分我并不是指望用 Bend 去写 OLED 驱动嵌入式底层永远需要 C、寄存器位操作和中断处理。但可以借鉴 Bend 强调的设计思路把状态机、边界、副作用隔离到尽可能小的范围。例如把 I2C 传输的时序建模成一个状态集合把“从任何错误状态都能回到初始状态”写成可检查的命题。如果某一天这种小型状态机的形式化验证变成日常工具那么代码审查中很大一部分“我猜这里可能出问题”的讨论就会变成“机器已经证明这里不可能出问题”。剩下的 review 时间就能花在硬件行为、实际时序和业务需求上。这才是 Lauren Tan 那句乐观判断真正有价值的地方。5. 我实际跑通 Bend 后的三个直接感受5.1 安装和第一个可并行程序我本地的环境是 Windows 自带的 WSL2 Ubuntu里面已经有 Rust 工具链。按照官方 README 推荐用 cargo 安装bend-lang然后写一个.bend文件。Bend 的安装命令和版本变化得比较勤建议以仓库当前说明为准。第一个程序我写了一个简单的递归计算def fib(n): if n 2: return n else: return fib(n - 1) fib(n - 2) def main(): return fib(20)然后用bend run跑它会在多核 CPU 上尽量并行。要上 GPU 可以用bend run-cu它会走 CUDA 后端。第一次跑的时候我开了 CPU 监控能明显看到多个核心同时被拉高而代码里没有任何线程库。这种体验确实和写普通 Python 时完全不同。5.2 从 C 语言思维切换到“返回新值”我写 C 的时间比较长最难受的就是习惯性想写循环。Bend 里想更新一个值只能生成一个新值。比如维护计数器不是counter 1而是把counter 1传给下一次递归调用。这种风格一开始会让人烦躁但配合不可变变量读代码时会明确感觉到一种安全感你不需要担心一个函数悄悄改掉了外部状态。更让我意外的是连错误处理都在往这个方向靠。Bend 里你没法说“把这个全局变量置为错误码”只能通过返回值把错误状态往上抛。代码里“错误路径”变少了但每一条路径都变得可追踪。这恰好也回应了标题如果代码都长成这样代码审查确实会轻松很多因为审查者面对的不再是充满隐藏副作用的黑盒而是一张清晰的数据流图。5.3 目前仍然存在的生态短板我也要吐槽几句。Bend 现在的调试体验不算好报错信息有时会直接暴露 HVM2 中间表示对普通用户很不友好。第三方库几乎为零想找一个 JSON 解析库或 HTTP 客户端都费劲。GPU 后端的调度细节也不够透明显存占用突然变得很高时你基本只能靠猜。另外小任务跑在 GPU 上反而比 CPU 慢。因为启动 CUDA、分配显存、来回搬运数据的开销可能比计算本身还大。我试过一个很小的递归求和bend run-cu比bend run-c慢了一个数量级完全不意外。所以现实一点讲Bend 现在更适合做算法原型验证、研究性项目或者作为探索可验证语言设计的测试场还不太适合直接上生产业务。6. 别急着下“审查被解决”的结论6.1 形式化验证验证的是程序不是业务意图代码审查不仅检查程序是否正确还检查程序是否满足了业务需求。机器只能证明“程序做了 X”至于 X 是不是业务想要的还是得人来判断。业务需求天然是用自然语言描述的充满歧义和取舍这些都不可能被编译成可验证的数学命题。所以即使 Bend 或者任何未来语言成熟到可以自动证明一堆不变量也替代不了产品和架构师的最终 review。它能够替代的是那种“是不是这里少了个判断”“是不是那里越界了”的低级但耗时的机械检查。把人的精力从机械检查里解放出来让人去面对真正的业务复杂性这才是“审查被解决”最合理的解释。6.2 最先受益的是哪些代码按我的经验最先受益的一定是规模小、状态模型清晰、逻辑陡峭的模块比如加密算法、协议解析、调度器、交易撮合规则。这类代码通常不长但错一个分支就致命。传统 review 看十遍也未必能保证正确形式化验证却可以证明所有可达状态都满足某条断言。反过来业务逻辑复杂的 CRUD 代码真正难的点在需求本身形式化验证帮不上太多忙。你不可能用一个定理证明器来证明“用户点了这个按钮之后弹窗文案符合运营预期”。所以我的判断是Bend 这种强调可验证性的语言形态会先从底层库、协议栈、驱动模块这类代码开始延伸而不是一上来就取代业务后端。6.3 我现在的看法绕了一圈回到标题。我现在觉得Lauren Tan 那句话最大的价值不是真的宣告代码审查被消灭而是把“可验证性”从学术讨论拉回了工程实践。代码审查不应该永远停留在“让人眼模拟执行”的阶段。语言今天提供类型检查明天提供更好的所有权和纯函数约束后天可能就提供内建的不变量证明。每一步推进都是在减少审查者需要盲猜的角落。Bend 是这条路线上一个很有意思的样本它用一套非常容易上手的语法让你提前体验了“不可变世界”里写代码和 review 代码分别是什么感觉。就算你最后不会在生产环境用它这种思考方式也值得保留。最后再分享一个小体会我最近做任何模块的设计评审时都会先问一句这段代码里哪些值是可变的哪些边界是隐含的能不能把隐含的边界变成语言能检查的类型这比单纯把代码读三遍有效太多。