全局属性的局部推理
本文探讨了如何通过局部推理（即仅关注代码的某一部分）来推导和维护系统的全局属性。作者分析了在复杂软件系统中，局部与全局推理之间的张力，并提出了几种实用策略，帮助开发者在不理解整个系统的情况下，依然能够确保关键全局属性的正确性。
背景速读
- 作者 Laurie Tratt 是编程语言领域的学者，本文讨论的是软件工程中的一个根本难题：如何通过局部代码推理（仅看一小段代码就理解其行为）来保证全局属性（整个程序的安全性、正确性等）。<br>- "局部推理"指程序员只看一个函数或模块就能搞懂它，不需要了解整个系统的状态；"全局属性"指类型安全、内存安全、并发无死锁等需要全程序分析才能保证的特性。<br>- 传统上这两个目标相互矛盾：局部推理容易但只能保证局部正确，全局属性需要全局分析又破坏了局部推理。文章通过 Rust 的所有权/借用系统和 Haskell 的纯度/单子（Monad）作为案例，展示如何在语言设计层面同时实现两者。<br>- 这是编程语言理论（PL）领域的经典问题，近年来因 Rust 等语言兴起而受到更多关注。