形式化验证学者 TaliaRinger：当年批评研究没用的人该道歉了

西北大学计算机科学教授 TaliaRinger 发帖称，多年来嘲笑验证与类型理论研究「没用」的人，如今大概该承认自己错了，甚至为「既刻薄又错了」道歉。随着 AI 代码生成兴起，形式化验证与类型系统对保障程序正确性的价值重新受到关注。