2026年9月18日，Bend 成为我关于振动编码一般观点的有用例子，因为它最近、高调，并且具有使其易于作为例子使用的方面。我不知道作者在设计语言方面的历史，或者他们是否真的考虑了下面的权衡并做出了我认为是糟糕的选择。随意将下面的“作者”替换为“可能创建相同事物的假设作者”。我显然不喜欢 Bend 中的设计决策，我想呈现这些决策，然而这已经被过度混淆为我下面试图表达的主要观点。我不想现在编辑这一点，使其看起来像任何现有评论被过度严厉，因此我认为最好的解决方案是解释我在撰写这篇文章时的心理模型是什么样子的。以下是 Bend 作者的一条评论。Bend 2 正被宣传为 AI 编码时代的语言：人类编写“定律”，AI 编写实现和证明，编译器检查证明是否健全。这听起来非常令人印象深刻，我也能理解为什么有人会想要这样的语言。然而，这个想法实际上存在一些主要问题；然而，这不是这篇文章的重点。相反，我想谈谈 Bend 本身似乎如何陷入了我很少看到被提及的振动编码常见陷阱。让我们从基准开始，看看 Bend 要求开发者为其主页演示编写什么：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 行代码。那么，我对此有什么问题？为什么我称其为振动编码陷阱？问题在于，振动编码使得在充分理解问题以认识到更好解决方案存在之前，就有可能构建出一个 substantial 解决方案。开发者可以在遗漏该领域入门调查本应直接呈现在他们面前的方法的情况下，构建出一种完整的语言和编译器。所涉及的领域是形式验证。值得注意的是，这两个词在 Bend 的网页或代码库中根本没有出现。开发者在似乎没有意识到该领域存在的情况下，构建了一种围绕该领域的完整语言。为了清楚地展示为什么这是一个问题，让我们重新创建 Bend 用作演示的相同程序，使用 SPARK，一个开源的形式验证语言和编译器。为了公平起见，我完全振动编码了这个程序，我只是告诉一个 LLM 用 SPARK 重新创建这个演示，没有进一步的指导：package Game with SPARK_Mode issubtype Column is Integer range 0 .. 11;subtype Row is Integer range 0 .. 7;type State is record X : Column; Y : Row; Won : Boolean;end record; Start : constant State := (8, 5, False);function Wall (X : Column; Y : Row) return Boolean is(((X = 3 or X = 11) and Y <= 3)or ((Y = 3 or Y = 7) and X <= 3));function Cell (X : Column; Y : Row) return Character is(if Wall (X, Y) then '#' elsif X = 1 and Y = 1 then 'F' else '.');-- Inductive invariant: outside the sealed room, off walls, not won.function Safe (G : State) return Boolean is((G. X > 2 or G. Y > 2) and not Wall (G.

X, G. Y) and not G. Won)with Ghost;procedure Step (G : in out State; Key : Character)with Post => (if Safe (G'Old) then Safe (G));-- Both Bend laws, including the actual cell drawn by the terminal.function Replay (Keys : St...