从 Bend 2 看氛围编码的陷阱：重造形式验证已有成果

作者评论 Bend 2 这种为 AI 编码时代设计的语言：其首页 demo 用 58 行"法则"和 442 行 LLM 证明代码来表达玩家无法获胜的性质。作者让 LLM 无额外指引地在形式验证语言 SPARK 中复刻同一 demo，运行 GNATprove 后全部 12 项检查通过，且无需从零构建长证明。