Bend 2 掉进了 Vibe-Coding 的陷阱
Bend 2 and the Vibe-Coding Trap
Bend 2 宣称是 AI 编程时代的语言，让人类写规则，AI 写代码和证明。但作者指出，其演示案例中，仅定义简单规则就需 58 行代码，而证明这些规则竟需 442 行。相比之下，使用成熟的 SPARK 语言重写相同逻辑，代码更简洁且证明过程高效。这正是 Vibe-Coding 的陷阱：开发者在缺乏领域知识的情况下，依赖 LLM 构建出看似可行实则落后数十年的方案，完全忽略了形式化验证领域已有的成熟标准。
Vibe-Coding 使得在尚未充分理解问题、未意识到存在更优方案之前，就构建出庞大解决方案成为可能。
HN 评论区
234- hmokiguess
问题在于，Vibe Coding 让人能够在对问题了解得还不足以意识到存在更优解之前，就构建出一个相当完整的解决方案。
抛开这个例子和 Bend 不谈，我发现这是我们面对当今所谓“智能”时最大的挣扎。它很擅长产出能跑的东西，但在指出你“不知道自己不知道”的事情时，它并不擅长。
除非你具备极强的自我意识和自律，否则它无法教育你或帮你纠正方向。
话虽如此，我认为这对所有事情都适用。陷入这个陷阱很容易，因为这是很人性的弱点。我们就是不知道自己所不知道的，所以重新审视旧方案，结果发现有了新信息可以将其替换为更好的方案，这种情况并不罕见。
我觉得这里没什么新东西，也没什么变化，如果有什么变化的话，只是我们经历这一过程的速度变了。LLM 让反馈循环变得更容易、更快速。
现在回到 Bend，我认为把你的作品公之于众，毫不避讳地展示出来，甚至开源，并愿意接受反馈，这将大有裨益。
我更担心的是那些正在被售卖且人们依赖的、基于 LLM 构建的闭源产品，它们无法获得来自众多思考者的这种宝贵批评。
- pu_pe
关于该项目的原始讨论（https://news.ycombinator.com/item?id=49746163）非常奇怪。里面有很多指责作者像个名人，还有各种随机账号为他背书，却几乎没有关于实质内容的讨论。
就连那个发布中的演示也没怎么跑通。
- z7
> 所涉领域是形式化验证（formal verification）。值得注意的是，这两个词在 Bend 的网页或其代码库中均未出现。开发者围绕一个似乎根本不知道其存在的领域构建了一整套语言。
我查了开发者的 X 账号，他写了很多关于形式化验证的帖子，所以这一具体说法（“似乎根本不知道其存在”）似乎是假的。
- thomasahle
> 这与 Bend 的不同之处在于，我们在这里提供的是证明程序正确性所需的一切，无需 LLM 浪费时间或 token 去从头构建一个 442 行的证明。我们可以运行 GNATprove 并得到：`Success: all checks proved (12 checks).`
GNATprove 使用 SMT 求解器，意味着它基本上是一个暴力证明系统。
是的，暴力证明比符号证明（lean, bend 等）更容易，因为你不需要提供证明。它完全是自动化的。
但暴力证明几乎无法扩展到任何有实际意义的内容，这就是为什么形式化验证在过去 30 年里一直是个小众领域，直到如今 LLM 能够编写真正的证明。
- johnfn
指责作者不懂形式化验证真是令人印象深刻，哪怕花几分钟做点研究就能立刻证明事实恰恰相反（https://x.com/victortaelin/status/2100942399132312059?s=46, https://x.com/victortaelin/status/2100374221671051472?s=46）。
- captainmuon
我还没细看 Bend 2，但称其“严重损坏或落后于当前最先进水平几十年”似乎有点过于苛刻。显然形式化验证语言确实存在问题，该领域确实需要别的东西，而问题在于可用性和语法。我不想学那种看起来像 Haskell 的东西，也不想费神去搞懂 Curry-Howard 对应关系。我不想用那种看起来和感觉起来都像 C++ 模板元编程的东西来写我的条件。我记得几年前有个类似 Coq 的 Hello World，基本上是从“首先，我们构建 Peano 整数”开始的，然后他们用这个来证明某个计算是有界的——看起来是因为他们无法原生表示整数？
我只想能够写 C#、JavaScript 或任何东西，然后用同样的语法附加前置条件、检查等等。让大众也能用上依赖类型和设计契约。
- mentalgear
> Bend 的作者完全忽略了这是形式化验证领域的当前标准，如果他们甚至知道这个领域存在的话。相反，他们搞出了这一整套需要冗长规范甚至更冗长证明的系统。在 Vibe Coding 整个语言和编译器之前稍微做点研究，本可以大幅提高结果，因为作者就会知道该要求什么。
> 这个例子的重要性超出了 Bend 本身。Vibe Coding 使得实现一个严重损坏或落后于当前最先进水平的方案变得太容易了，因为你可以在不进行任何研究的情况下立刻得到结果。如果你让 LLM 构建一种语言，使其能够通过从头构建证明来证明函数的形式正确性，它会乐意照做，它绝不会停下来建议你：电脑已经可以构建复杂证明，无需 LLM 介入，并能消除 99% 的工作。它绝不会告诉你，你正在构建的东西大部分已经存在，你可以在此基础上进行开发。
---
这就是为什么你所有要求构建实质性内容的 LLM 请求都应该以“先进行前期工作研究”开始。当然，在某个阶段一切都会收敛（如果我们开源分享输出），那时我们可能会有坚实的标准模式和库，无需在全球范围内浪费数万亿 token 去重复重建同样的微小基础事物，每个人都在自己的沉默中重造轮子 […]
- wg0
README.md[0] 中一些值得注意的行：
> - 编译器（非内核）99% 由 AI 编写，尚未完全审计。
> - 字符串是字符链表，因此文本处理很慢。