主要观点：如今 Rust 讨论多围绕内存安全，但其重点是程序正确性。
关键信息：

• 形式语言理论：语法与语言、语义紧密相关，C 存在未定义行为，编译器假设部分代码不可能，导致难以预测结果。
• 运行时异常非解决方案：多数现代语言处理异常方式不佳，难以知道操作何时引发异常及是否必须处理所有异常。
• 使无效状态不可表示：正则表达式示例表明语言应定义所有可能输入的输出，Rust 专注于程序正确性，借调检查器确保引用有效，避免无效程序。
• 软件工程作为一门技艺：软件开发应遵循明确步骤，重视正确性，如 CompCert 经形式验证的 C 编译器几乎无 bug。

重要细节：

• 形式语言中语法与自动机、语义双向关联，C 抽象机可建模 C 程序执行。
• 现代语言在处理异常方面存在诸多问题，如 Java 的未检查异常、Python 等不提示函数可能引发异常等。
• Rust 通过借调检查器等特性使编写正确软件更易，且其关注点不仅在于内存安全。
• 软件开发应重视步骤 1 到 2，即定义解决问题的方法并确保抽象机遵循计划，而步骤 3 常被忽视，如 CompCert 经多年验证几乎无 bug。