主要观点：成功的软件也是有缺陷的软件，不能仅依赖程序能工作就认为其正确，需警惕成功，遵循“对成功保持怀疑”（BSOS）原则。
关键信息：

• 模型检查时，未发现违反活性属性或安全属性错误都应存疑，代码需因正确原因工作。
• 处理“对成功保持怀疑”的常用方法是验证，如测试、静态检查等，但也应怀疑验证的成功，测试应先写失败的测试用例。
• 主流验证方法擅长解释失败原因，而成功不如失败信息丰富，可通过“让它工作，让它失败”来判断代码是否因正确原因工作。
• 相关话题“快乐路径和悲伤路径”，代码在快乐路径工作良好不代表在悲伤路径也能工作，应同样保持怀疑，如处理超时的重试机制等。
  重要细节：
• 有论文指出 35%的灾难性分布式系统故障由“错误处理程序中的琐碎错误”引起。
• 推荐博客 Red Blob Games，其内容主要是关于计算机游戏编程，但有通用计算机科学算法的交互式指南，如 A*算法介绍、噪声函数概述等，其博客文章可订阅。
• Jimmy Koppel 曾提出代码变体有“超属性”。
• 作者的新书《Logic for Programmers》已进入早期访问，可获取。