Szegedy 预测 2030 年主流软件将全部被形式化验证

Google 研究员 Christian Szegedy（sytelus）重申其坚持十年的预测：数学对世界最大的影响不是千禧年难题，而是大规模软件证明——到 2030 年所有主流软件都将被形式化验证，用户不会再接触未经验证的库，规格形式化和十亿行级代码验证将成为现实。该预测引发激辩，有观点认为遗留技术债务是实现这一愿景的最大障碍。

2026-09-21 ~ 2026-09-22 · 3 条相关