主打“为 AI 时代而生”的编程语言 Bend 2 最近遭遇了一场尖锐的技术审视。独立开发者 Liam Powell 在分析其官方示例时指出，Bend 2 试图用大模型从第一性原理手动构建证明的做法，恰恰踩中了所谓的“氛围感编程（Vibe-Coding）陷阱”——开发者借助大模型的高速生成能力，在完全没有调研形式化验证（Formal Verification）成熟生态的情况下，用极高的 token 代价重新发明了一个效率极其低下的轮子。
这起技术争议的价值远不止于一行代码的优劣。它展现出当前 AI 辅助开发中最典型的系统性风险：工具的易得性抹平了工程无知带来的阻力，让设计者在缺乏领域常识的情况下快速堆砌出整套基础设施，却在底层留下了难以弥合的正确性断层。
442 行归纳与 12 次求解：一次代差悬殊的技术对照
Bend 最初由 HigherOrderCO 团队推出，早先以交互网（Interaction Nets）为基础主打自动大规模并行。进入 Bend 2 阶段后，该项目转向主打规格与证明的闭环开发逻辑：由人类开发者定义规律（laws），AI 编写具体的实现与证明，再交由编译器完成严格验真。
在这套看似严密的闭环中，官方仓库提供了一个名为 app_win_is_bug_2d 的游戏演示。开发者在 LAWS.bend 中用 58 行代码声明了两项基础法则：在任意按键序列下游戏永远无法获胜，且玩家坐标永不能落在显示为“F”的旗帜单元格上。然而，为了让系统证明这一简单的不可达性质，大模型在 PROOF.bend 中被迫从基本原理出发，手写了 442 行证明代码。
对比之下，若将相同的判定逻辑移植到工业界成熟的形式化语言 SPARK（Ada 的验证子集）中，开发者只需写清状态约束与循环不变量，底层的 GNATprove 验证工具就会自动调用 SMT 求解器放行全部 12 项检查。整个过程不需要让语言模型反复推导几百行归纳证明，也不需要消耗昂贵的算力。
在形式化方法领域，自动求解技术早在数十年前就已成为软件工程的常规武器。Bend 2 错位的地方在于，它在完全可以由 Z3 或 CVC4 等 SMT 求解器自动判定的一阶逻辑状态问题上，让大模型去模仿 Coq 或 Lean 极其繁重的高阶证明项推导。
氛围感编程让开发者在看清成熟解法之前，就过早完成了一整套残缺的实现。
掩盖在代码行数之下的编译器隐患
如果只是证明繁琐，问题依然停留在开发效率层面。深入该项目的实际代码与更新记录会发现，Bend 2 面临的更严峻挑战来自形式化语义与编译器实现之间的脱节。
形式化验证的立足之本在于整个验证链条的完全可靠（Soundness）。只要证明检查器通过，生成的二进制程序就绝不允许出现预期外的行为。但目前的 Bend 2 在这层根基上存在明显的结构性缺陷：
在代码注释与官方说明中，Bend 团队坦承其基于 Lean 构建的形式化规范尚未与实际编译器实现完全对齐，代码库中依然留存有 @unsafe 绕过标记和未经审计的逻辑。这意味着它宣称的“由编译器验真保证法则不破”，在数学推导层面目前缺乏端到端的坚实担保。
更为具体的工程缺陷直接表现在近期公开的 Issue 中。Issue #800 指出，Bend 2 存在严重的跨环境符号绑定歧义：当代码中存在外部函数的重复定义时，JavaScript 后端会选择静默接受并直接篡改前向调用，而 C 语言后端则会严格报错拒绝。这种前后端执行逻辑的分裂表明，检查器（Checker）通过的性质无法在所有运行目标中等价生效。此外，Issue #791 记录了有效程序因检查器自身的递归限制而被判定非法的案例。
前端给出了繁复严密的数学假象，后端却带着未受控的执行漏洞。当核心编译器无法杜绝符号劫持与语义偏差，前端耗费数百行推导出的证明就会在运行时瞬间归零。
- 风险.当语言验证器无法在多端输出中维持严格的语义同一性，依赖 AI 生成的证明不仅无法提供安全保障，反而会演变成高危的防御盲区。
计算机科学基本盘：生成速度无法替代的认知纵深
Bend 2 的困境是当前整个软件工程界正在经历的技术缩影。在 LLM 具备强大代码生成能力的当下，写出一个能运行的语法解析器、解释器甚至玩具编译器，已经变成一个下午就能完成的“氛围感编程”实验。
但语言模型本身不具备知识体系的全局批判力。如果开发者只向大模型索求“如何用纯逻辑推导一个循环证明”，AI 就会极其顺从地吐出长达几百行的递归证明项。它不会主动提示开发者：四十年前就有一门叫作 SPARK 的语言，可以用成熟的 SMT 求解器把这一切压缩到毫秒之间。
- 建议.对于计划在安全关键系统引入 AI 验证工具的团队，应优先选择以 SMT 自动化求解为骨干的成熟框架，而非让 LLM 在生产环境裸写脆弱的证明项。
在 AI 编码时代，撰写代码的边际成本已经趋近于零。决定系统终局高下的，不再是谁能用提示词快速搭起庞大的语法骨架，而是开发者是否具备扎实的计算机基础认知，能否在架构定型前识别出现有工业界的成熟方案。缺乏底层审慎的狂奔，产出的不过是带着现代包装的旧时代遗存。