北京
一个编程语言的主页演示，要求开发者先写大量代码，只为声明"玩家永远碰不到旗子、永远赢不了游戏"。然后，AI需要再写更多代码，来证明这些法则确实成立。
这是Bend 2展示给外界的样子。它被包装成"AI编程时代的语言"：人类写"法则"，AI写实现和证明，编译器检查证明是否可靠。听起来很完整，很自洽。
但问题恰恰藏在这个自洽里。
氛围编码让人先造出答案，再发现题目早就有人解过
氛围编码有一个隐蔽的副作用：它让开发者能在真正理解问题之前，就搭出一套相当完整的解决方案。一个人可以造出一整门语言和编译器，却错过一个入门级综述就会直接摆在眼前的现成路径。
这个路径叫形式验证。
值得注意的是，"形式验证"这四个字，在Bend的网页和代码库里一次都没有出现过。开发者围绕一个领域造了整门语言，却似乎没有意识到这个领域本身已经存在。
这不是在指责某个人。换成任何一个在同样信息条件下动手的人，都可能掉进同一个坑。氛围编码降低了动手的门槛，却没有同步抬高"先做功课"的门槛。
同样的演示，换一种语言重写一遍
为了把问题说清楚，可以拿Bend主页那个演示程序，用SPARK重做一遍。SPARK是一门开源的形式验证语言和编译器。
做法很直接：告诉一个大模型，用SPARK把这个演示复刻出来，不给任何额外指导。结果是一段完整的SPARK代码，包含状态定义、墙壁判定、单元格绘制、安全不变量，以及一个带后置条件的回放函数。
这段代码里，两个Bend法则都被覆盖了，连终端实际绘制的单元格都考虑在内。它把证明程序正确性所需的一切都写在了同一处，不需要让大模型从零开始，一行一行堆出冗长的证明。
跑一遍GNATprove，输出是：
- Success: all checks proved
- 12 checks
12项检查，全部通过。
差别不在聪明程度，在有没有先看一眼地图
Bend的做法是：先写一套冗长的规格说明，再写一套更冗长的证明。法则和证明的比例悬殊。
SPARK的做法是：把法则和证明所需的信息放在一起，让验证工具直接跑。没有额外的冗长证明，也没有让大模型把时间花在从第一性原理重建证明上。
这不是说SPARK一定适合所有场景，也不是说Bend的每一条设计决策都错了。差别在于，Bend的作者似乎完全错过了形式验证领域当前的标准做法——如果他知道这个领域存在的话。
他造出的是一套需要冗长规格、还需要更冗长证明的系统。而这套系统要解决的问题，在另一个领域里已经有更成熟的答案。
氛围编码真正的陷阱，是让人跳过"这题有没有人做过"
氛围编码的吸引力在于，它让"从零到一"变得前所未有地容易。你不需要先成为领域专家，就能让大模型帮你把想法变成可运行的东西。
但"从零到一"容易了，"从一到更好"反而更难被发现。因为当你已经用氛围编码造出一整套东西，你会倾向于继续在这套东西上迭代，而不是回头问一句：这个领域里，有没有人已经给出了更简洁的解法？
Bend的例子之所以典型，是因为它足够新、足够高调，也足够容易拿来当样本。它不是一个孤例，而是一种正在变得常见的模式：先动手，后理解，最后才发现自己重造了别人早就验证过的轮子。
形式验证不是新东西。SPARK也不是新东西。GNATprove跑出12项检查全部通过，也不是什么惊人的结果。真正让人意外的，是这些现成的东西，在一门号称面向AI编程时代的语言里，连名字都没有被提起过。
氛围编码不会替你判断方向。它只会沿着你给的方向，飞快地跑下去。方向错了，跑得越快，离答案越远。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
