Thomas 预言：两年内多数代码将用 Lean4 编写，产物比 Rust 更快

Thomas 预测，两年内大部分代码将用 Lean4 或同等形式化语言编写，最终二进制将比 Rust 或 C 更快。他认为，AI 将大幅降低形式化验证成本，促成内置智能并采用激进优化的编译器架构。