Bend 2 与 vibe-coding 陷阱：在调研之前造完了一门语言和编译器

Bend 只是一个方便的例子，用来讲我对 vibe-coding 的一般看法：它新、受关注、而且很容易拿来说明问题。我对作者设计语言的历史一无所知，也不知道他是否真的权衡过我下面说的取舍、并做出了在我看来不算好的选择。你可以把下文的「作者」替换成「一个可能做出同样东西的假想作者」。

我显然不喜欢 Bend 的设计决策，并且想把这些讲出来，但这被过度地和本文想表达的要点混在一起了。我不想现在改动文章、让已有评论显得过于苛刻，所以我觉得最好的办法是说明我写这篇文章时的思路是怎样的。

这里是 Bend 作者的一条评论。

Bend 2 正被宣传成一门「面向 AI 编码时代」的语言：人写「law（定律）」，AI 写实现与证明，编译器检查证明是否成立。听起来相当厉害，我也能理解为什么会有人想要这样一门语言。这个想法其实有几个重大毛病；不过那不是本文的主题。我想谈的是 Bend 本身如何掉进了 vibe-coding 的一个常见陷阱，而这个陷阱我很少看到有人提起。

先看看 Bend 首页那个 demo 要求开发者写什么作基线：

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 的网页和代码库里一次都没有出现过。开发者似乎是围绕一个领域造出了整门语言，却没意识到这个领域存在。

为了清楚地说明为什么这是个问题，我们把 Bend 用作 demo 的同一个程序，用 SPARK——一门用于形式化验证的开源语言与编译器——重做一遍。为对 Bend 公平起见，这段我完全是 vibe-code 出来的：我只让 LLM 用 SPARK 复现那个 demo，没有给任何进一步指引。

package Game with SPARK_Mode is
   subtype 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 : String) return State
     with Post => not Replay'Result.Won
       and Cell (Replay'Result.X, Replay'Result.Y) /= 'F';
end Game;

------------------------------

package body Game with SPARK_Mode is
   procedure Step (G : in out State; Key : Character) is
      X : Column := G.X;
      Y : Row := G.Y;
   begin
      case Key is
         when 'w' => Y := (Y - 1) mod 8;
         when 's' => Y := (Y + 1) mod 8;
         when 'a' => X := (X - 1) mod 12;
         when 'd' => X := (X + 1) mod 12;
         when others => return;
      end case;
      if not Wall (X, Y) then
         G := (X, Y, G.Won or Cell (X, Y) = 'F');
      end if;
   end Step;

   function Replay (Keys : String) return State is
      G : State := Start;
   begin
      for Key of Keys loop
         pragma Loop_Invariant (Safe (G));
         Step (G, Key);
      end loop;
      return G;
   end Replay;
end Game;

------------------------------

with Ada.Text_IO; use Ada.Text_IO;
with Game; use Game;

procedure Main is
   G : State := Start;
begin
   Put_Line ("Winning is impossible. WASD + Enter to move; q + Enter to quit.");
   loop
      for Y in Row loop
         for X in Column loop
            Put (if X = G.X and Y = G.Y then 'P' else Cell (X, Y));
         end loop;
         New_Line;
      end loop;
      Put_Line (if G.Won then "WON (this should be unreachable)" else "still not won");
      exit when End_Of_File;
      declare
         Keys : constant String := Get_Line;
      begin
         exit when Keys = "q";
         for Key of Keys loop
            Step (G, Key);
         end loop;
      end;
   end loop;
end Main;

现在我们用 Bend 同样的方式定义了那些定律。我想说明的到底是什么？

与 Bend 的差别在于：这里我们给出的，已经包含证明程序正确性所需的一切，而不需要让 LLM 浪费时间和 token，从基本原理出发搭出一份 442 行的证明。我们可以运行 GNATprove，得到：

Success: all checks proved (12 checks).

Bend 的作者完全错过了这一点：这已经是形式化验证领域的现行标准——如果他确实知道这个领域存在的话。他反而造出了一整套需要冗长规格、以及更加冗长证明的系统。在 vibe-code 出一整门语言和编译器之前做一点调研，本可以大幅改善结果，因为作者会知道该向 AI 要什么。

这个例子意义超出 Bend 本身：vibe coding 让「实现一个糟糕透顶、或落后当前技术水准几十年的设计」变得太容易，因为你不做任何调研就能立刻拿到结果。如果你向 LLM 要一门「可以通过从基本原理搭证明来证明函数形式正确」的语言，它会很乐意照做；它永远不会停下来提醒你：计算机早就能在不借助 LLM 的情况下构建复杂证明，并且可以消掉 99% 的工作量。它也永远不会告诉你：你想造的东西，大部分已经以「可以在此基础上继续做的工作」的形式存在了。