关键信息：

• 希尔伯特计划被哥德尔、丘奇和图灵的工作推翻，表明数学不能完全理解所有事物，计算机程序能被形式推理但不能被完全理解。
• 停机定理表明不存在判定任意程序是否终止的算法，其有多个直接推论，如关于可达性、莱斯定理等，还引出“忙碌海狸定理”，体现分析程序复杂性的困难。
• 计算机科学与数学关注不同范畴，程序本质上与完全理解、证明和正确性相悖。
• 计算复杂性理论诞生，时间层次定理表明计算问题存在无限的难度层次，有界停机问题等也证明了一些问题的固有难度。
• 软件验证是计算机科学中最困难的问题，限制机器或性质的方法都不能使验证更易，语言抽象在验证中一般不能被利用，不存在普遍可验证的编程语言。
• 介绍多种软件验证方法，如模型检查、演绎证明、抽象解释和类型系统等，各有优缺点，且都受计算复杂性的限制。

重要细节：

• 图灵认为计算与物理过程相关， Church-Turing 论题认为任何物理过程的计算都可由 Church 和 Turing 描述的通用计算模型完成。
• 哈特曼尼斯和斯特恩斯通过有界停机问题证明时间层次定理，哥德尔可能也使用了类似思想。
• 各种限制条件下的验证尝试，如总语言、有限状态机等，都无法使验证更易。
• 模型检查受状态爆炸问题影响，演绎证明可针对特定问题更具可扩展性但成本高，抽象解释通过不精确性避免复杂度问题，类型系统与抽象解释相关等。
• 最后呼吁计算机科学应采取实证主义方法，通过对人类编写程序的经验研究来解决验证问题。