https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/LAWS.bend
我不打算在这里复现代码，因为代码本身并不太重要。对本文而言，重要的是这段代码相当长。仅仅为了声明玩家永远无法触碰旗帜或赢得游戏，就需要整整58行代码。这里还存在其他问题，比如 LLM 可以重新定义 Game 子程序来做任何事情；不过，这同样不是本文的重点。
接下来看看 LLM 为这个程序编写代码时，需要写出什么才能证明这些"法则"：
https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/PROOF.bend
相当庞大。足足442行代码，只为证明那些简单的性质。
那么我对这有什么不满呢？为什么我称其为 vibe-coding 陷阱？
问题在于，vibe coding 让人能够在充分了解问题、足以识别出存在更优解决方案之前，就构建出一个规模可观的解决方案。开发者可以在完全错过一种入门级领域综述就会直接呈现在眼前的方案的情况下，产出一整套语言和编译器。
这里所说的领域就是形式化验证（formal verification）。值得注意的是，这两个词在 Bend 的网页或代码库中完全没有出现。这位开发者围绕一个领域构建了一整套语言，却似乎没有意识到该领域的存在。
为了清楚地说明为什么这是一个问题，让我们用 SPARK——一种用于形式化验证的开源语言和编译器——来重现 Bend 用作演示的同一个程序。公平起见，说明一下：这段代码完全是我 vibe-coded 出来的，我只是让 LLM 在 SPARK 中重现这个演示，没有给出任何进一步的指导：