主要观点：作者因教授 TLA+ 工作坊下周无 newsletter，分享对形式方法的思考，重点是系统建模中的非确定性。
关键信息：

• 形式方法是主要收入来源但多数读者不用，故多分享其思想。
• 非确定性分为五种：真随机性、并发、用户输入、外部力量、抽象。
• 真随机性多数时候是伪随机，形式语言常将其视为非确定性选择。
• 并发是最显著的非确定性来源，很多形式语言有特殊语法处理并发。
• 用户输入的程序可能有无限输出，长期系统对用户输入的建模可体现非确定性。
• 外部力量如读取外部传感器等也会导致非确定性和不确定性。
• 抽象可隐藏确定性过程的实现细节，简化系统建模和对错误的敏感性。
  重要细节：
• 如在一个咨询项目中，机器接收消息后进入三种状态，其最终状态由消息内容决定但过程复杂，被抽象为非确定性选择。
• 提到《C 程序设计语言》中第一个非确定性程序的例子。
• 解释了对非确定性的一些思考及相关著作、书籍等信息。