本德 2（Bend 2）被宣传为AI编程时代的语言：人类写规则，AI写实现与证明，编译器检查证明可靠。作者不想讨论理念问题，而是指出本德本身陷入了少被提及的vibe-coding常见陷阱。以主页演示为例，开发者需写不少代码，仅声明玩家不能碰旗帜或赢游戏就用58行。虽大语言模型可重定义Game子程序，但重点不在此，接下来看LLM为证明规则需写什么。

Bend 2（https://bend-lang.com/）被宣传为 AI 编程时代的语言：人写“法则”，AI 写实现和证明，编译器检查证明是否正确。这听起来不错，理解有人想要这样的语言。不过这不关其他问题，我们要谈的是 Bend 自身似乎陷入了一个少被提及的 vibe-coding 陷阱。

Bend 主页演示要求开发者写的“法则”代码（https://github.com/bendlang/bend/blob/main/demos/appwinisbug2d/LAWS.bend）有 58 行，仅仅声明玩家永远不能碰旗子或赢游戏。LLM 还能重定义 Game 子程序做任意事，但这不是重点。

LLM 为证明这些“法则”需要写的代码（https://github.com/bendlang/bend/blob/main/demos/appwinisbug2d/PROOF.bend）长达 442 行，来证明那些简单属性。

问题何在？vibe-coding 陷阱在于：它在人足够了解问题前就能建成庞杂方案，错过更好的解法。开发者能做出整门语言和编译器，却错过了该领域入门综述就会指出的方法。

这领域是形式化验证。Bend 网页和代码库里连“形式化验证”二字都没出现。开发者围绕该领域建了整门语言，却似乎不知其存在。

为展示问题，作者用 SPARK（开源形式化验证语言）让 LLM 完全靠 vibe-coding 重现同一演示，无额外指导。生成的代码包含状态、墙函数、安全不变量、步骤过程等，十分简短。运行 GNATprove 得到：“Success: all checks proved (12 checks).” 这样我们提供了证明程序正确所需的一切，而不用 LLM 从第一原理浪费时间构建 442 行证明。

Bend 作者完全错过了这是形式化验证领域的当前标准（若他知晓该领域存在）。他搞出整套需要冗长规范和更冗长证明的系统。在 vibe-coding 整门语言前做点调研，本可大幅改进结果，因为作者会知道该要什么。

这例子超越 Bend：vibe-coding 让人太容易实现糟糕或落后数十年的设计，因为能立刻出结果而不调研。若让 LLM 造一门语言，能从基本原理建证明来形式验证函数，它会照做，却绝不会建议计算机已能自动建复杂证明省 99% 工作，也不会说你造的东西大多已作为可借鉴成果存在。

多数人质疑 Bend 是未审计、蹭热度的 vibe-coded 落后语言，少数人（含作者）强调其十年形式验证功底与为性能故意设计的冗长证明，分歧主轴在作者对领域认知及形式验证语言应否大众化。

认为作者不懂形式验证且 vibe-coded 出落后语言

• 质疑者称 Bend 作者完全错过形式验证现行标准，所需规范与证明极其冗长，属于未做研究便用 AI 拼凑未审计编译器；原讨论多吹捧作者少实质且 demo 不佳，更有指其明知标准却蹭热点刷星，除生成 C 外无独特想法。（认可度：较多人） > 作者整门语言与编译器都是 vibe-coded，忽略了形式验证领域早已存在的自动证明方案（@LiamPowell）

认为作者深谙形式验证且设计取舍合理

• 作者本人及支持者指出其研究该领域近十年，发布过相关演讲与依赖类型实现；Bend 证明冗长是为数十倍提升类型检查速度的有意选择，AI 可填充证明如汇编般无需人读。查证其社交账号也证伪“不知领域存在”说。（认可度：较多人） > 我花十年研究形式验证，Bend 的冗长证明是故意换类型检查速度，AI 工具能自动补证明（@LightMachine）

认为形式验证语言亟需易用性革新而非简单否定

• 有意见认为批评 Bend“破碎落后”过于苛刻，现有证明语言语法晦涩（如 Haskell 风、模板元编程），大众渴望用熟悉语法（C#/JS）附加契约，依赖类型应平民化。（认可度：少数人） > 形式验证的痛点是语法可用性，人们只想用日常语言写代码再直接加前置条件（@captainmuon）

认为 LLM 辅助须先检索先验艺术否则重复造轮子

• 多位指出 LLM 不会主动告知已有成果，用户必须养成先令其调研领域现状的习惯；懂得“问什么”才是核心价值，机器易奉承用户已找到完美方案。（认可度：较多人） > 若记得让搜索型 LLM 先梳理先验工作，能省下大量重复造轮子的时间（@simonw）

认为手写形式规范成本过高，AI 生成测试证明才是实际出路

• 底层算法外多数软件写验证规范不现实，但现代模型已能写普通测试供人略读；大型证明达数万行，AI 辅助不可或缺。（认可度：较多人） > 为大多数软件手写形式规范验证代价过高，但新模型写测试已够用（@IshKebab）

社区将争议视作久违的娱乐戏剧

• 有人调侃自 2019 V 语言后未见的发布争议，视为比 AI 新闻更有趣的谈资。（认可度：少数人） > 很高兴终于有新戏剧可追，比 AI 新闻好看（@assumed_throwaw）

有价值的补充

• 代码本身即你想要应用的规则最紧凑的表示（@GodelNumbering）
• 面向 LLM 的语言应可交互如 Lisp，而非编译型（@vegnus）
• 若证明由 AI 生成且无人阅读，它将如同生成汇编般成为隐形层（@LightMachine）
• 程序合成研究如 SupGen 在文献基准上已超越约十倍性能（@LightMachine）