Bend是一种新的编程语言，编译为原生代码和GPU，以Python风格语法提供接近C的性能。它采用Lean/Rocq式的证明检查类型系统来防止AI生成代码的错误，允许用户声明编译器强制执行的不变量规则。主要特性包括快速编译、跨核心和GPU的自动并行化，以及形式化验证支持。
背景
Bend针对AI编程代理日益普及后对可靠AI生成代码的需求。该项目将形式化验证作为在编译时防止AI编程错误实用工具引入。
- 来源
- Lobsters
- 发布时间
- 2026年9月18日 16:15
- 评分
- 6.0 / 10
Bend是一种新的编程语言，编译为原生代码和GPU，以Python风格语法提供接近C的性能。它采用Lean/Rocq式的证明检查类型系统来防止AI生成代码的错误，允许用户声明编译器强制执行的不变量规则。主要特性包括快速编译、跨核心和GPU的自动并行化，以及形式化验证支持。
Bend针对AI编程代理日益普及后对可靠AI生成代码的需求。该项目将形式化验证作为在编译时防止AI编程错误实用工具引入。