主要观点：

• 人们对形式化方法的最大担忧是能否用规格说明生成代码，担心实施规格说明时出错有 bug 以及实现会“偏离”且不更新规格说明导致意外设计问题。
• 使代码与规格同步有两种方式，即程序提取和细化，但同步成本高，会损失抽象层次，对大多数公司来说难以承受。
• 尽管不能同步，规格说明仍有价值，有规格说明时在生产中出现 bug 能更准确诊断和修复，能更快构建和修复系统。
• 正在研究从规格说明生成代码和测试的方法，如 PGo 将 PlusCal 转换为 Go 代码，MongoDB 从 TLA+规格说明生成测试用例等，但仍有局限性。

关键信息：

• 形式化方法中人们常问能否用规格生成代码及相关担忧。
• 同步代码与规格的两种方式及各自特点和成本。
• 有规格说明在生产中诊断和修复 bug 的优势。
• 正在研究的从规格生成代码和测试的工作及现状。

重要细节：

• PlusCal 是编译为纯 TLA+的领域特定语言，举例说明规格比代码更抽象。
• 以 AWS SQS 为例说明规格可包含系统及环境。
• 介绍 PGo 将 PlusCal 转换为 Go 代码及示例。
• MongoDB 从 TLA+规格生成测试用例的过程及相关工具。
• 对“An assumption in the design was wrong”问题的说明。
• 关于订阅、主要网站及新书信息。