Bend 2 掉进了 Vibe-Coding 的陷阱

Bend 2 and the Vibe-Coding Trap

Bend 2 宣称是 AI 编程时代的语言，让人类写规则，AI 写代码和证明。但作者指出，其演示案例中，仅定义简单规则就需 58 行代码，而证明这些规则竟需 442 行。相比之下，使用成熟的 SPARK 语言重写相同逻辑，代码更简洁且证明过程高效。这正是 Vibe-Coding 的陷阱：开发者在缺乏领域知识的情况下，依赖 LLM 构建出看似可行实则落后数十年的方案，完全忽略了形式化验证领域已有的成熟标准。