Bend
3 hours ago
- Bend是一种快速的编程语言，它结合了类似C语言的性能、CUDA级别的并行性和类似Lean的证明检查，以防止AI错误。
- 它使用LAWS.bend文件声明不变性定律，并使用PROOF.bend文件正式证明这些定律成立，从而在使用正确时，从数学上杜绝了错误。
- Bend编译为原生代码，在单核上运行时几乎与C一样快，并可扩展到16核或GPU（最高可达100倍加速），无需显式的线程或锁管理。
- 它的类型检查器兼作证明检查器，但比Lean或Rocq快得多（不到一秒），使得AI代理能够在每次更改后验证代码。
- 该语言是为后AGI经济设计的，允许人类通过定律和证明向AI指定精确、无歧义的需求，而不是手动读写代码。
- 使用LAWS.bend，AI必须重试直到构建出定律成立的证明；合并错误是不可能的——它变成了一个定理。
- 实际用法包括运行'bend guide'进行学习，使用LAWS.bend定义关键规则，以及在提交前运行'bend PROOF.bend'。
- Bend还很年轻，在Linux/macOS后台上运行效果最佳，鼓励用户报告错误，并在出现问题时让AI提交问题。