形式化验证为什么这么难：从停机问题到每天四行代码的证明工程困境
1969年，Tony Hoare发表了一篇只有三页的论文，提出了后来被称为"Hoare逻辑"的形式系统。他在论文开篇写道：“计算机程序员总是要和程序正确性打交道。“半个多世纪过去了，程序员们依然在和程序正确性打交道——只是我们选择的方式，几乎从未真正拥抱过Hoare的方案。 ...
1969年，Tony Hoare发表了一篇只有三页的论文，提出了后来被称为"Hoare逻辑"的形式系统。他在论文开篇写道：“计算机程序员总是要和程序正确性打交道。“半个多世纪过去了，程序员们依然在和程序正确性打交道——只是我们选择的方式，几乎从未真正拥抱过Hoare的方案。 ...