Bend 2 踩了 vibe coding 的坑：没调研就造了一门语言，结果被 SPARK 零行证明打脸

Bend 2 and the Vibe-Coding Trap

Liam Powell 拿 Bend 2 的官方 demo 开刀，指出 vibe coding 最大的坑：你可以在完全不了解一个领域的情况下，靠 AI 把整套方案都写出来。Bend 2 的 demo 要证明玩家永远赢不了，需要 AI 生成 442 行证明代码。Powell 用现成的形式化验证语言 SPARK 重写了同一个 demo，编译器自动完成所有正...