bend

Bend 2 是一种为后 AGI 时代设计的新编程语言，在这个时代，人类通过无歧义的语言向 AI 系统传达意图。其核心创新是 LAWS.bend——一种机制，开发者在此声明不变量（法则），AI 必须数学证明任何代码更改都满足这些法则，从而在数学上不可能合并违反这些规则的错误。 README 中展示的关键能力： **性能**：在 CPU 上达到 C 级速度，在 GPU 上达到 CUDA 级速度。基准测试显示单核性能具有竞争力，并在数千个核心上实现大规模并行扩展。编译器利用强类型、纯函数性和线性特性进行优化。 **证明检查**：声称验证速度比 Isabelle、Agda、Lean 或 Coq 快数个数量级，可在不到一秒内检查复杂证明。 **隐式并行**：无需编写线程、锁或内核。分治函数自动分布在所有可用的 CPU/GPU 核心上。示例显示 pow2(20) 分布在 4,096 个 GPU 核心上。 **AI 协作工作流**：专为 AI 辅助开发设计。开发者用 LAWS.bend 编写法则（例如，“余额总和必须为零”、“玩家不能穿过墙壁”），然后要求 AI 在提交前运行 `bend PROOF.bend`。编译器机械地强制执行证明。 **语言特性**：类似 Python 的语法，支持依赖类型。仿射/线性类型系统（值不能共享）。需要终止递归（带有 @unsafe 转义）。目标平台包括 C、Metal、CUDA、JavaScript。基础库最小化；效果包括 I/O、通道、TCP/UDP、文件访问。 **当前限制（明确列出）**：注释冗长，无类型类/特质/宏，无策略或证明搜索，数值类型有限（仅 Nat、U32、F32），字符串慢（链表），无 HTTP/JSON/TLS/正则表达式，每个程序仅支持单个 GPU，无增量编译，原生编译慢，工具链最少（无 LSP、调试器、格式化器、REPL），编译器主要由 AI 编写且未经审计。 该项目包括 Lean 中的形式化（bend.lean）、学术论文（BendTT 类型理论、BendRT 运行时）以及不断增长的演示集合。社区渠道：Discord、Reddit、X/Twitter。提供的材料中未指定许可证。