Bend 2 与氛围编程的陷阱

# Bend 2 与氛围编码陷阱 来源：https://blog.liampwll.com/posts/bend_vibe_coding/ 2026年9月18日 Bend 2 (https://bend-lang.com/) 被宣传为面向人工智能编码时代的编程语言：人类编写"法则"，人工智能实现算法与证明，编译器则负责验证证明的有效性。这听起来相当令人印象深刻，我理解为何有人会想要这样一门语言。然而，这个想法存在几个主要问题；不过，本文并不讨论这些。相反，我想谈谈 Bend 自身似乎已陷入一个常见的氛围编码陷阱，这一点我鲜少见到有人提及。 让我们先看看 Bend 在其官网演示中要求开发者编写的基础内容： https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/LAWS.bend 我不会在这里复现代码，因为代码本身并非重点。对本文而言重要的是，这段代码相当冗长。仅仅是声明"玩家永远无法触碰旗帜或赢得游戏"，就需要 58 行代码。此外还存在其他问题，例如大语言模型可以随意重定义 `Game` 子程序来执行任何操作；然而，这同样不是本文的重点。 接下来，让我们看看大语言模型为编写此程序的证明代码需要写些什么： https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/PROOF.bend 这段代码非常庞大。需要 442 行代码来证明那些简单的性质。 那么，我对它有什么不满？为什么我称之为氛围编码陷阱？ 问题在于，氛围编码使得开发者在深入了解问题、认识到存在更优解决方案之前，就能构建出一个庞大的解决方案。开发者可能会不遗余力地打造一门完整的语言和编译器，却忽略了一项在领域入门综述中本应直接呈现的方法。 此处的领域指的是形式化验证。值得注意的是，"形式化验证"这两个词在 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 '.'); -- 归纳不变式：在密封房间外、远离墙壁、且未获胜。 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)); -- 两条 Bend 法则，包括终端实际绘制的单元格。 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 ("胜利是不可能的。使用 WASD + 回车移动；输入 q + 回车退出。"); 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 "胜利了（这本应是不可达的）" else "仍未获胜"); 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 不同的是，我们这里提供的内容足以证明程序的正确性，无需让大语言模型浪费时间和算力从基础原理构建一个 442 行的证明。我们可以运行 GNATprove 并得到： `` Success: all checks proved (12 checks). `` Bend 的作者完全没有意识到，这是当前形式化验证领域的标准做法，更不用说他们是否知道这个领域的存在。相反，他们提出了这个整套系统，要求冗长的规范和更加冗长的证明。在氛围编码构建整门语言和编译器之前，稍作研究本可以大幅改进结果，因为作者会知道应该寻求什么。 这个例子的重要性超越了 Bend 本身。氛围编码使得实现一个设计极其糟糕或落后于当前技术水平数十年的方案变得过于容易，因为你可以立即获得成果而无需进行任何研究。如果你要求大语言模型提供一门能够从基本原理构建证明来形式化验证函数正确性的语言，它会欣然接受，却绝不会停下来建议你：计算机已经能够无需大语言模型就能构建复杂证明，从而消除 99% 的工作。它绝不会告诉你，你正在构建的东西，大部分已经作为可继承的基础而存在。