「串台」故障的原因终于揭晓；吴涛的莫尔斯码 app 主意看来目前不可行；三封很长的读者反馈；主题是设计模式。两位主持人不约而同地病了，所以没有讲新闻。

节目中提及的读者 Haozhong Zhang 来信节选：

相对的，在 Formal Verification 中，举个例子，我们可以把每条指令的执行形式化表示成 {P}C{Q}，其中 C 是这条指令，P 称为前条件 (Pre-condition) 描述了 C 执行之前机器的状态 (例如某个寄存器的值是什么，某个内存单元的值是什么，通常不需要覆盖所有的寄存器和内存单元，仅需要根据验证的 Specification 选取我们关心的部分), Q 称为后条件 (Post-condition) 描述了 C 执行后的机器状态。注意，这里 Q 同时描述 C 被中断和不被中断的执行后的机器状态。非形式化的，{P}C{Q} 表示在满足前条件 P 的机器上执行指令 C 得到的机器状态满足后条件 Q。这样，对于上述的一个代码片段 C1; C2; …; CN 我们有 {P1}C1{Q1}，{P2}C2{Q2}, …, {PN}CN{QN}。然后，我们证明 Q1 ⇒ P2, …, QN-1 ⇒ PN，