Bend 2 和 Vibe-Coding 陷阱

Bend 2 和 Vibe-Coding 陷阱 2026 年 9 月 18 日 [Bend 只是我的观点的一个有用的例子。我对作者设计语言的历史一无所知，也不知道他们是否确实考虑了下面的权衡并做出了我认为是一个糟糕的选择。] Bend 2 被定位为人工智能编码时代的语言：人类编写“法律”，人工智能编写实现和证明，编译器检查证明是否可靠。这一切听起来相当令人印象深刻，我可以理解为什么有人会想要一种能够做到这一点的语言。这个想法实际上存在一些主要问题；然而，这不是本文的主题。相反，我想谈谈 Bend 本身如何陷入了振动编码的常见陷阱，但我没有看到太多提及。让我们从 Bend 要求开发人员在主页上为其演示编写的基线开始：https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/LAWS.bend 我不会在这里重现它，因为代码不太重要。对于本文来说，重要的是它有相当多的代码。 58行代码只是为了声明玩家永远不能碰旗帜或赢得游戏。还有其他问题，LLM 可以重新定义游戏子程序来执行任何操作；然而，这又不是本文的重点。接下来让我们看看为该程序编写代码的法学硕士需要编写什么才能证明“定律”：https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/PROOF.bend 这很多。 442行代码证明了这些简单的属性。那么我对此有什么问题呢？为什么我称其为振动编码陷阱？问题是，在充分了解问题并认识到存在更好的解决方案之前，vibe 编码可以构建一个实质性的解决方案。开发人员可以生成完整的语言和编译器，但却缺少该领域的介绍性调查直接摆在他们面前的方法。所讨论的领域是形式验证。值得注意的是，这两个词没有出现在 Bend 的网页或其代码库中。开发人员似乎围绕一个领域构建了整个语言，但没有意识到该领域的存在。为了清楚地说明为什么这是一个问题，让我们重新创建 Bend 在 SPARK 中用作演示的相同程序，SPARK 是一种用于形式验证的开源语言和编译器。为了公平起见，我完全对此进行了振动编码，我只是告诉法学硕士在 SPARK 中重新创建演示，没有进一步的指导：包 Game with SPARK_Mode 是子类型 Column is Integer range 0 .. 11 ；子类型 Row 是整数范围 0 .. 7 ；类型 State 是记录 X : Column ； Y：行；赢得：布尔值；结束记录；开始 : 常量 状态 := ( 8 , 5 , False );函数 Wall ( X : Column ; Y : Row ) 返回布尔值是 ((( X = 3 或 X = 11 ) and Y <= 3 ) 或 (( Y = 3 或 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 '.' ); -- 感应不变量：在密封的房间之外，离开墙壁，不能赢得。函数 Safe(G: State) 返回布尔值是 ((G.X > 2 或 G.Y > 2) 而不是 Wall (G.X, G.Y) 并且不是 G.Won) 和 Ghost； procedure Step ( G : in out State ; Key : Character ) with Post => ( if Safe ( G ' Old ) then Safe ( G )); -- 两个弯曲定律，包括终端绘制的实际单元格。函数 Replay(Keys: String) 返回 State with Post => not Replay 'Result。 Won and Cell(重播'结果.X,重播'结果.Y)/='F';游戏结束； ------------------------------ 包体 SPARK_Mode 的游戏是程序步骤（G：处于out状态；Key：字符）是X：列：= G。 X; Y：行：= G。是; begin case 关键是 ' w ' => Y := ( Y - 1 ) mod 8 ;当 ' s' => Y := ( Y + 1 ) mod 8 时；当 ' a ' => X := ( X - 1 ) mod 12 时；当 ' d ' => X := ( X + 1 ) mod 12 时；当其他人=>返回时；最终情况；如果不是 Wall ( X , Y ) 则 G := ( X , Y , G . Won 或 Cell ( X , Y ) = ' F ');结束如果;结束步骤；函数 Replay(Keys: String) 返回 State 为 G : State := Start ；开始 for Key of Keys 循环编译指示 Loop_Invariant ( Safe ( G ));步骤（G，键）；结束循环；返回 G ；结束重播；游戏结束； ------------------------------ 与 Ada.Text_IO ；使用 Ada.Text_IO ；与游戏；使用游戏；程序主要是 G : State := Start ; begin Put_Line("不可能获胜。WASD + Enter 移动；q + Enter 退出。");在行中循环 Y 在列中循环 X 循环 Put ( if X = G . X and Y = G . Y then ' P ' else Cell ( X , Y ));结束循环；新行；结束循环； Put_Line ( if G . Won then "WON (this should be unreachable)" else " still not win" );当 End_Of_File 时退出；声明 Keys : 常量 String := Get_Line ;当 Keys = "q" 时开始退出； for Key of Keys 循环步骤 ( G , Key );结束循环；结尾 ;结束循环；主要结束；现在我们已经定义了与弯曲相同的定律，我在这里想表达的意义是什么？这与 Bend 的不同之处在于