全局属性的局部推理

- 作者 Laurie Tratt 是编程语言领域的研究者，长期关注语言设计与实现中的工程挑战。本文讨论的是软件工程中一个经典难题：如何通过局部的代码修改来保证全局系统行为正确。 - "局部推理"（local reasoning）指的是程序员只需看某一段代码就能理解其影响；"全局属性"（global properties）则是整个程序必须满足的不变量或约束。现代大型系统里，局部修改往往意外破坏全局行为，导致难以追踪的 bug。 - 文章分析了几种典型场景（如状态共享、并发控制、依赖注入等），并比较了不同编程语言和范式（函数式、面向对象、类型系统）在支持局部推理方面的优劣。 - 核心观点在于：语言设计如果能将全局约束显式编码（例如通过类型系统或所有权模型），就能让开发者在局部代码中直接推理全局正确性，减少心智负担和运行时错误。