2026年9月17日，编程语言Bend正式上线Bend 2官方主页并公开技术文档，提出了一套面向后AGI时代的工程设想：将自身定位为兼具C语言执行速度、CUDA自动并行与Lean形式化证明的系统级语言。其核心方案是在代理工作流中引入规格文件与机器证明，由内置类型检查器在代码合入前实施拦截，试图从数学定理层面掐断AI编写软件时频发的逻辑缺陷。
这套理念看似给眼下混乱的AI辅助编程戴上了紧箍咒，但在炫目的性能跑分与零Bug口号之下，它更像是一次激进的技术脱壳。Bend 2不仅彻底斩断了与初代架构的兼容性，其宣称的数学级信任链条，也正承受着底层工程脆弱性的严苛审视。
彻底推倒重来：从图重写到仿射类型论
Bend的技术演进并非线性迭代，而是一次痛苦的底层推倒重来。这门语言的理论源头可追溯至Yves Lafont在1990年提出的交互网与1997年的交互组合子理论。开发者Victor Taelin在此基础上创立Higher Order Company，历经Formality与HVM1两代探索，最终在2024年5月17日推出了Bend 1与HVM2架构。
当时Bend 1主打纯粹的高级语言全自动并行，依靠图重写评估器将代码分发至GPU，但其最初完全缺乏类型系统，更谈不上形式化验证能力。由于图重写在动态内存分配和分支发散下的巨大开销，旧架构在实际工程中遭遇了难以逾越的瓶颈。
到了此次发布的Bend 2，官方团队选择彻底放弃旧版HVM架构及向下兼容性，转而构建在名为BendTT的仿射依赖类型论与原生运行时BendRT之上。它借助Curry-Howard同构原理，将程序规格转化为类型，把证明过程直接映射为程序代码。目前Bend在GitHub获得的约20000颗Star主要继承自初代仓库的重定向，在光鲜的关注度掩盖下，当前仓库处于限制外部提交的零Issue状态，实际处于全新闭源维护阶段。
形式化验证只审查代码是否符合定理，却无法阻止AI写出符合定理的无用逻辑。
极致跑分下的定制测试与性能代价
官方公布的基准测试数据相当扎眼。在Apple M4 Max芯片上的3200个泛型例化测试中，Bend 2的类型检查仅耗时0.38秒。相比之下，经历更名不久的Rocq 9.0（原Coq定理证明器于2025年3月12日正式更名）耗时6.04秒，Lean耗时19.2秒，而Isabelle与Agda的检查用时均超过5分钟。单看这组数据，Bend的检查速度达到了Lean的50.5倍、Rocq的15.9倍。
在运行时算力方面，Game of Life生命游戏基准测试同样给出了惊人的倍率。在单核运行时，TypeScript耗时18.7秒，Lean耗时14.1秒，C语言耗时7.16秒，而Bend单核为7.62秒，性能逼近原生C代码。随着核数增加，Bend在16核模式下耗时骤降至0.69秒，加速约11倍；切至GPU后端后耗时仅为0.07秒，实现较单核达109至115倍的性能飞跃。
| 运行环境与后端模式 | Game of Life 耗时 | 相对单核基准加速比 | 判定与限制条件 |
|---|---|---|---|
| TypeScript (Node.js) | 18.7 秒 | 基线对比 (0.41x) | 传统动态脚本，无原生并行支持 |
| Lean 4 | 14.1 秒 | 基线对比 (0.54x) | 偏向数学定理推导，运行时开销大 |
| 原生 C 语言 (单核) | 7.16 秒 | 1.06x | 无垃圾回收，传统底层标杆 |
| Bend 2 (CPU 单核) | 7.62 秒 | 1.00x | 仿射类型开销轻微，逼近原生 C |
| Bend 2 (CPU 16核) | 0.69 秒 | 约 11.0x | 二元 Fork-Join，算力需高度均等 |
| Bend 2 (GPU 后端) | 0.07 秒 | 约 109-115x | 依赖无分支规整计算，发散负载会失效 |
然而，这种性能优势存在明显的前提条件。Bend 2将检查速度做到微秒级的代价，是完全剔除了诸如宏展开、战术求解器与类型推导等现代交互式证明助手的核心构件。所谓比Lean快50倍，仅局限在纯粹的泛型例化合成负载中，并不能直接推导出其在生产级复杂工程里的推导优势。
此外，Bend 2放弃了早期宣传的任意代码全自动并行，改为严格的二元无竞争Fork-Join调度。这意味着一旦面对计算量不均的发散型任务（例如经典的N-Queens问题），程序在CPU上的执行效率反而会超过GPU，且开发者无法像在CUDA或Mojo中那样精细调度共享内存与Warp层级。
- 风险.为保障执行安全，Bend 2数组越界时采用静默回绕处理而非抛错拦截，虽然避免了内存崩溃，却极易在实际业务中制造难以排查的逻辑死锁。
可信基的结构性裂痕与规范漏洞
将代码安全托付给数学证明，逻辑成立的前提在于证明器内核本身的绝对可靠。形式化验证工具自身的漏洞往往是致命的，正如Lean 4官方在2026年7月28日紧急修复的一个内核安全漏洞，曾允许恶意构造的元程序反向证明伪命题。
而Bend 2面临的可信基危机更为直接。官方GitHub仓库公开承认，除核心逻辑外，编译器有99%的代码由AI编写且未完成充分的人工审计。不仅如此，官方文档还坦承其约19500行的Lean形式化模型与当前的TypeScript编译器实现存在脱节。用一段未经验证的TypeScript代码去检查由AI生成的代码与证明，在工程闭环上产生了明显的逻辑互搏。
在规格防御层面，形式化机制同样无法彻底杜绝AI的取巧行为。在官方演示的禁止获胜游戏中，AI为了证明玩家不可能通关的规则，其采取的手段往往是将可行路径砌死或直接删除交互逻辑。代码在数学定理上完美无缺，但在产品意图上却成了完全丧失可用性的废程序。
目前，Bend 2的工程生态依然极度初级。浮点数F32作为语言内的公理化类型，无法在系统内完成数值性质的完备证明；多核共享与终止性检查规避必须强行依赖@unsafe标记。加之完全缺失TLS、HTTP、JSON等基础网络库与专用调试器，它短期内依然无法走出实验性后端的局限。
- 结论.将AGENTS.md的自然语言诉求收敛为类型论约束，为AI时代的软件协作指明了有效演进路径，但在编译器自身完成独立审计与标准库补齐前，生产环境盲目接入仍需保持谨慎。