局部推理保证全局属性

# 关于全局属性的局部推理 来源：https://tratt.net/laurie/blog/2026/local_reasoning_for_global_properties.html 在过去几年中，我越来越多地被问到这样一个问题：AI 是否会受益于新型编程语言？我的回答一直是“可能不会”，而且至少到目前为止，这个回答依然成立：AI 现在已经能够在你我能想到的几乎任何编程语言中生成大量代码。但随着技术不断进步，其特性也变得越来越清晰，我的看法也发生了变化。根据我的经验，AI——至少目前如此——通常能生成高质量的局部代码（例如一个函数），但在需要生成要求对整个程序有全局理解的代码时，却经常遇到困难。最容易观察到这一点的现象就是大量不必要的防御性检查：这些检查看似无害，但却可能导致程序后续阅读者认为可能出现的状态数量呈指数级增长，从而带来一系列不良后果。也许这种困难很快就会被克服，但如果没有，我们或许会再次从编程语言设计中寻求帮助。本文的目的并非试图预测编程语言将（甚至应该）以何种具体方式来解决这个问题¹。相反，我想回答一个更基本的问题：我们是否有这样一个良好的编程语言设计范例，它允许通过局部推理来确保某个令人惊讶的全局属性？ ## 背景 我的很大一部分收入来自于编程语言，因此我有切身利益去强调它们的重要性。然而，尽管我认为编程语言确实对我们的生产力以及所创建软件的可靠性有一定影响，但并没有太多证据表明它们能产生根本性的差异。我的意思不仅仅是“没人能设计出一个好的实验来证明差异存在”——尽管这确实是真的！更准确地说，很多“好”的软件是用“差”的语言创建的，而很多“差”的软件却是用“好”的语言创建的。特定编程语言似乎不太可能是这类结果的主要影响因素。对此最简单的论证是：创建能够满足用户所有需求、并且可理解、可靠的软件，需要更多的同理心，而非对挑战性编程语言特性的精通。如果要说更细致一些的观点，我之前曾尝试阐述我对软件本质的思考（https://tratt.net/laurie/blog/2024/what_factors_explain_the_nature_of_software.html）。 这不应被理解为我认为编程语言**毫无**作用。当我从汇编语言转向 Python 和 C 这样的“高级”语言时，我的生产力大幅提升，并且觉得自己能够应对更大的软件项目。原因很简单：汇编语言迫使我处理太多底层细节，以至于我常常忘记更重要的高层全局图景。我能创建的软件质量差异是巨大的。但不幸的是，我逐渐意识到这种巨大的改进不太可能再次出现。我缓慢而笨拙地重新发现了弗雷德·布鲁克斯的“没有银弹”论点（https://www.cs.unc.edu/techreports/86-020.pdf）： > 过去软件生产率的大部分重大提升都来自于消除人为障碍，这些障碍使得偶然性任务变得异常困难，例如严苛的硬件限制、笨拙的编程语言、缺乏机器时间。现在软件工程师所做的工作中，还有多少是专注于偶然性而非本质性的？除非偶然性工作占总工作量的 9/10 以上，否则把所有的偶然性活动都缩减到零时间也带不来数量级的改进。 ## 一个例外 这意味着，在很多很多年之后的某个特定背景下，当我再次体验到我所编写的大量软件在生产力上发生了深刻变化时，我惊讶得几乎没注意到。当我终于意识到这一点，并试图向他人解释这种差异时，他们似乎也感到困惑。这个背景是什么？就是 Rust 中的多线程编程。正是这段经历影响了我对编程语言未来发展方向的看法，所以我需要说服你：Rust 使多线程编程变得更容易的方式中蕴含着某种深刻的东西。 让我从具体例子开始。我编写了构建你现在正在阅读的网站的程序，它原本是普通的单线程代码。因为我比较懒——而且我的网站也没那么大——每次运行时都会重建整个网站。过了一段时间，我发现重建网站的暂停时间已经长到足以让编辑某些页面（比如本文！）变得低效。我迅速做了一些单线程优化，但还不够。于是我猜想，如果能重写为多线程，就能把暂停时间降到可接受的水平。在几乎任何其他编程语言中，重写软件以使用多线程都是一项艰巨的任务。事实上，我过去的多线程经验告诉我，我会立刻遇到难以调试的崩溃；而且几乎肯定，在数周乃至数月内还会遇到一连串这类可怕的问题。我早就放弃了尝试编写多线程程序，这完全合理！然而在这个特定案例中，重写——确实解决了性能问题——只花了不到 5 分钟。它第一次运行就正确，并且一直保持正确——而且我对此完全充满信心。这怎么可能呢？ 我非常喜欢 Rust——自 2015 年以来它一直是我的主要语言——但它并非完美的语言。实际上，我可以（也确实）通过详细剖析其缺陷来让人厌烦。但在多线程方面，它做到了我从未想象过的事：数据竞争（https://doc.rust-lang.org/nomicon/races.html）（即未协调的读/写，两个线程可能意外地相互干扰）变成了静态错误。这可不是小事：以前，当我试图编写多线程程序时，数据竞争是错误的最大来源²。 ## Rust 如何防止数据竞争 Rust³ 通过所有权类型以及 `Send` 和 `Sync` trait 的结合来防止数据竞争。如果你了解 Rust 的工作原理，可以跳过这一节。如果你不了解 Rust，我将尽可能简短地概述这些特性，并尽量简化。所有权类型可能会让人迷失，但我们只需要知道：每个对象都有一个所有者，可以对其进行读写；对象可以转移给其他所有者，之后原所有者失去对该对象的访问权，而新所有者获得访问权。 `Send` 意味着“此结构体的实例可以从当前线程移动到另一个线程”（即移动后当前线程无法访问该对象）。`Sync` 意味着“多个线程可以同时读取此结构体的实例”。为简化起见，我们可以假设 Rust 会自动判断一个结构体何时可以安全地实现 `Send` 和/或 `Sync`，并自动为我们实现这些 trait。 我们先看这段非常简单的 Rust 代码： ```rust fn main() { let x = vec![1, 2]; println!("{x:?}"); } ``` `vec!` 创建的向量是 `Vec` 类型的实例，它实现了 `Send`。因此我们可以将一个向量发送到另一个线程，让那个线程打印出该向量： ```rust fn main() { let x = vec![1, 2]; std::thread::spawn(move || println!("{x:?}")).join().ok(); } ``` `std::thread::spawn(...)` 是在 Rust 中创建新线程的方式：`move || ...` 是一个“闭包”（即匿名函数），新线程在启动时会运行它。`move` 意味着新线程成为外部函数中引用的任何数据的拥有者（即 `x` 被移动到新线程）。`join` 意味着主线程等待新线程结束。 我们可以看到主线程确实失去了对向量的访问，因为这段代码： ```rust fn main() { let x = vec![1, 2]; std::thread::spawn(move || println!("{x:?}")).join().ok(); println!("{x:?}"); } ``` 会导致如下编译时错误： ``` error[E0382]: borrow of moved value: `x` --> t.rs:4:14 | 2 | let x = vec![1, 2]; | - move occurs because `x` has type `Vec<i32>`, which does not implement the `Copy` trait 3 | std::thread::spawn(move || println!("{x:?}")).join().ok(); | ------- ------- variable moved due to use in closure | | | value moved into closure here 4 | println!("{x:?}"); | ^ value borrowed here after move | help: consider cloning the value before moving it into the closure | 3 ~ let value = x.clone(); 4 ~ std::thread::spawn(move || println!("{value:?}")).join().ok(); | error: aborting due to 1 previous error For more information about this error, try `rustc --explain E0382`. ``` 我甚至还没引入完整的数据竞争，Rust 就已经阻止我做坏事了！错误建议我们 `clone` 值：有经验的 Rust 程序员会对这个建议持谨慎态度，因为它可能导致性能极差。 为什么不尝试用引用计数类型 `Rc` 来包装对象呢？这样我们就能在两个线程间愉快地共享这个值了： ```rust fn main() { let x = std::rc::Rc::new(vec![1, 2]); std::thread::spawn(move || println!("{x:?}")).join().ok(); println!("{x:?}"); } ``` 但不幸的是，这会导致如下错误： ``` `Rc<Vec<i32>>` cannot be sent between threads safely ``` 我们不能将 `Rc` 实例移动到另一个线程的原因是引用计数没有以线程安全的方式实现。幸运的是，有一个变体可以做到这一点：“原子引用计数” `Arc`。出于一些稍微乏味的原因，我需要克隆 `Arc`（幸运的是，它不会克隆内部的向量！）： ```rust fn main() { let x = std::sync::Arc::new(vec![1, 2]); let y = std::sync::Arc::clone(&x); std::thread::spawn(move || println!("{y:?}")).join().ok(); println!("{x:?}"); } ``` 这段代码编译并成功运行：两个线程都从同一个向量读取并打印相同的内容。 最后，让我们尝试通过引入 Rust 的标准 `RefCell` 类型来启用跨线程的共享可变性： ```rust let x = std::sync::Arc::new(std::cell::RefCell::new(vec![1, 2])); ``` 我们再次得到错误，但这次不是关于*发送*（`Send`），而是关于*共享*（`Sync`）： ``` error[E0277]: `RefCell<Vec<i32>>` cannot be shared between threads safely ... = help: the trait `Sync` is not implemented for `RefCell<Vec<i32>>` ``` 可以说这是我们第一次真正尝试引入一个完整的数据竞争：Rust 再次阻止了我们。如果我想跨线程启用共享可变性，我需要引入像 `Mutex` 这样的类型： ```rust fn main() { let x = std::sync::Arc::new(std::sync::Mutex::new(vec![1, 2])); let y = std::sync::Arc::clone(&x); std::thread::spawn(move || { y.lock().unwrap().push(3); println!("{:?}", y.lock()); }).join().ok(); println!("{:?}", x.lock()); } ``` 这段代码编译并正确运行（打印出两次 `1, 2, 3`）。 ## 全局推理的扩展 至此，我希望读者已经感受到 Rust 能阻止我在程序中引入数据竞争。需要强调的一点是，Rust 并没有真正引入新特性来实现这一点：只需要所有权类型以及 `Send` 和 `Sync` trait 就够了。换句话说，我写的仍然是“正常”的 Rust 程序；我不必像编写 `async` 程序时那样使用新的子语言。因为 Rust 中有利于多线程程序的规则，对于有经验的 Rust 程序员来说既自然又明显，这可能会阻止我们观察到更深层的真相：Rust 以一种我可以在局部进行推理的方式，对我的程序强制实施了全局的无数据竞争属性。 例如，这个属性是在函数签名层面强制实施的： ```rust fn f<T>(x: T) { std::thread::spawn(move || println!("{x:?}")).join().ok(); } fn main() { f(vec![1,2]); } ``` 由于我没有约束 `T`，Rust 无法确定调用 `f` 时传递给 `f` 的是一个可 `Send` 的对象，因此第 2 行的 `spawn` 会导致如下错误： ``` `T` cannot be sent between threads safely ``` 要让这段代码正常工作，`f` 必须要求其调用者传递的对象确实允许发送到其他线程。语法有些笨拙： ```rust fn f<T>(x: T) where T: Send + 'static { std::thread::spawn(move || println!("{x:?}")).join().ok(); } fn main() { f(vec![1,2]); } ``` 现在确实可以编译并运行了！好消息是，通过查看 `f` 的签名，我确切地知道调用它不会在 `x` 上引起数据竞争。因此，这段代码片段因为使用了 `Rc` 而编译失败： ```rust f(std::rc::Rc::new(vec![1,2])); ``` 但如果我改为： ```rust f(std::sync::Arc::new(vec![1,2])); ``` 它就能编译通过。 ## 为什么全局推理如此强大 对于那些不熟悉 Rust 的读者来说，你们会很高兴地知道代码片段到此为止。我展示这么多例子的原因是，我希望你现在相信以下陈述：所有权类型、`Send` 和 `Sync` 的结合意味着我可以在只查看局部代码的情况下，全局地推理多线程和数据竞争的影响。 这听起来可能像是一种普通的静态类型保证：毕竟，如果我编写（比如）一个 Haskell 程序，我保证在运行时不会出现类型错误。这是没错，但 Haskell 普通的类型系统本身并不能像 Rust 那样保证并发代码没有数据竞争。换句话说，在 Rust 之前，我默认假设标准编程语言能够在不带来过多痛苦的情况下强制实施的唯一全局属性就是“没有运行时类型错误”⁴。我以为必须使用异域和/或实验性语言才能实现这样的属性，并且所涉及的权衡折中很少程序员能够接受。Rust 的无数据竞争保证是准确的，违反规则时的错误（大部分）是可理解的，并且整体结果非常实用⁵。 ## 未来的语言 我们现在可以回到最初的话题。让编程即使是在中等规模的程序上也变得困难的原因是，每次局部修改都像一只蝴蝶——而这些蝴蝶的翅膀扇动会在远处引起巨大的风暴（即 bug！）。这始终是个问题：即使是最优秀的人类程序员也难以获得并维持对他们所编写软件的全局视图。而目前，AI 常常更加困难。让 AI 生成一个具有清晰规范定义的单个函数，它通常能创造出比我更好的代码，而且速度更快。让 AI 生成一个中等规模的软件然后进行改进，结果往往不尽如人意。人们经常谈论代码膨胀，虽然这确实存在，但忽略了更深层次的问题：系统的全局视图往往被笨拙地、有时甚至错误地捕捉在生成的代码中。 最容易（尽管绝不是唯一！）观察到这个问题的方式是，AI 生成的代码往往包含大量*防御性检查*。断言和防御性检查有时会被混为一谈，但它们非常不同。断言在观察到意外情况时会立即终止程序：它们表达的含义是“如果这个条件不成立，说明程序员误解了系统的运行方式，或者系统的其他部分出了问题”。而防御性检查则不会终止程序：即使检查失败，执行也会有意继续。因此，防御性检查更适合理解为“我不确定这个条件是否成立，但如果它确实失败了，我希望用一种优雅的方式来处理它”。防御性检查看似