Why Rust solves a Problem we no longer have – use AI and Formal Proofs instead
4 months ago
- #AI
- #Formal Methods
- #Rust
- 文章指出，随着AI技术的兴起，当前通过Rust语言强调内存安全的做法已经过时。
- AI能够生成可编译为C语言的正式规范（如Event-B/B方法），通过数学证明确保系统无缺陷。
- 高级编程语言的设计初衷是降低人类认知负荷，但AI不需要这些限制，因为它不存在人类的易错性。
- B方法（如巴黎地铁14号线项目所采用）通过数学方式证明系统正确性，但过去因操作难度大难以普及。
- AI可自动化形式化验证过程，实现从经过证明的模型直接生成正确C代码，无需人工干预。
- 交通信号灯系统的案例研究表明，AI+Event-B通过不变量保障安全性，而Rust仅能防范内存错误。
- 结论建议将焦点从用Rust重写代码，转向利用AI进行形式化证明并精确表达系统意图。