2026 年 9 月 18 日
本文讨论的重点是 Bend 语言的设计思路，以及它所暴露的「vibe-coding」常见问题。作者本人对这门语言的设计历史并不了解，文中引用的一切均以「一位假设的作者」为讨论对象，而非针对具体个人。
Bend 被宣传为面向 AI 编码时代的语言：人类负责编写「规律」（laws），由 AI 编写实现和证明，编译器则负责验证证明是否正确。这一愿景可以理解，但其设计决策存在明显问题。
以下从 Bend 官方仓库主页演示所要求开发者编写的基本代码开始分析：
https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/LAWS.bend
这段代码本身不值得逐行复述，真正值得注意的一点是它的体量：代码量相当大，而玩家实际上永远无法触旗或赢得游戏。另一个已知问题是 LLM 可以重新定义游戏子程序并任意改写行为，但这并非本文的讨论范围。
再看 LLM 为证明上述「规律」所需编写的代码：
https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/PROOF.bend
问题在这里变得具体：仅仅是证明几个简单的属性，就需要 442 行代码。
这被称为「vibe-coding 陷阱」的原因在于：在对问题领域有充分了解之前，完全有可能构建出一个实质性的解决方案——一位开发者可以独立完成一门完整的语言及其编译器，却始终不知道相关领域的成熟方法已经存在。
这个领域就是形式化验证（formal verification）。值得注意的是，在 Bend 的网页和代码库中，「形式化验证」一词均未出现。开发者在似乎并未意识到该领域存在的情况下，围绕它从零构建了一门完整的语言。
为了说明问题所在，可以用 SPARK 重建 Bend 演示中使用的同一个程序。以下实现仅由指令「在 SPARK 中重做该演示」直接生成，没有提供任何进一步指导：
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 再消耗时间和算力去编写 442 行证明。直接运行 GNATprove 即可得到：
Success: all checks proved (12 checks).
用详细的规范取代冗长的手写证明，正是形式化验证领域现行的标准做法，而 Bend 的设计似乎完全没有参考这一既有成果。在动手编写完整的语言和编译器之前进行一些基础调研，本可以显著改善最终结果。
这一案例的意义也超出了 Bend 本身：vibe-coding 使得构建一个糟糕或落后几十年的设计变得轻而易举。当需求被表述为「设计一门能通过证明来验证函数正确性的语言」时，LLM 会照单全收地执行，乐于从零推导一切；它不会主动指出计算机完全可以在没有 LLM 参与的情况下自动生成复杂的证明、从而消减 99% 的工作量，也不会提醒用户所构建的东西早已作为成熟方案存在。
