与其他命令式语言相比，Rust 类型系统和避免共享可变状态两个特性可以实现更好的本地推理和形式验证。
局部推理
- 局部推理重要性：它能在不考虑整个程序状态的情况下验证程序属性。
- Rust 的所有权模型和没有可变别名比其他语言更有利于局部推理。
对形式验证进行扩展
- 虽然完整的形式验证很难，但Rust 已经证明了基于编译器的验证是值得的。
- 如果可以以较少的成本添加更多内容，就应该这样做。
Rust 将开发工作量转移到左侧
- 编译 Rust 代码是一种形式化验证，有助于更早地发现错误（“左移”）。
- 虽然并非所有程序都能得到完全验证，但验证某些程序的某些属性是有价值的。
原文摘要：
在 Rust 1.0 发布九周年之际，其创建者 Graydon Hoare 现身并撰写了一篇博客文章，扩展了without.boats 的另一篇文章。
你看，这些聪明的人正在努力解决一个问题：如何最大限度地发挥语言的静态分析能力和可用性？
Rust 迈出了一大步。但人们还想要更多：
剧透：答案是结构化并发。
- 结构化并发是将线程限定在实际上下文范围内，而不仅仅是父对象或某物。
- 甚至会限制结构化并发，这样线程集/子集/其他任何东西都不是语言的首要概念（非一流）。
Leakpocalyspe
Leakpocalyspe是一个只有高级 Rustaceans（和像我这样的语言迷）才认识的术语，我怀疑它在 Rust 1.0 左右团队成员的心里占有特殊的位置。
但是，如果 Rust 不能保证析构函数会被调用，那么某些 API 实际上是不安全的。
为何Rust不保证析构函数被调用？
- 这个月是 Rust 1.0 发布九周年，九年前也就是 2015 年 5 月。发生了 Leakpocalypse 的 bug。
- 如果您在 2015 年 4 月加入 Rust 团队，那么您只有不到两个月的时间来解决可能导致安全代码变得不安全的设计问题！
- 由于时间不足，需要走捷径，所以最终的决定是Rust 不保证调用析构函数。
我认为这在当时是正确的决定；
- 为了保证 Rust 的安全，故意泄漏内存似乎是一件小事。
- 但是，这意味着 Rust 不是最优的。
Rust成功原因
Leakpocalypse 并没有夺走 Rust 最大的成功。尽管我讨厌 Rust，但我当然承认它比我最喜欢的可用语言 C 有了很大的进步。
Graydon Hoare 和我认为 without.boats 正确地指出了 Rust 成功背后的原因：“shared-xor-mutable（共享可变状态）”规则。
- Rust 最大的成功并不是借用检查器，而是 shared^mut 。
- 但是，shared^mut增加了复杂性。
这主要是增加设计的复杂性，一旦你了解了模式，就很容易开始适当的设计。有点像 Rustaceans 改变他们的设计习惯来满足借用检查器。
rust 避免共享可变状态具有深远的影响；
当我们在 Rust 中形式验证程序时，我们可以使用 FOL 并避免分离逻辑，因为类型系统保护我们免受可变别名的影响，而 caml 中的情况并非如此，尽管它是“函数性的”
如果我只编写不会泄漏线程的函数会怎么样？
- 假设你有一个函数。该函数启动一个线程，然后返回。
- 函数返回后，新线程继续运行。
- 新线程泄露了：线程从函数中泄漏出来。
异步也会泄露：
- 异步函数返回 Future 或 Promise，即代码最终将在稍后执行的承诺。
- 函数返回后，子程序中的代码也还将执行。
- 异步也会从函数中泄漏出来。
Rust async 一书中提到了另外三种方法：
- 事件驱动编程，但如果没有其他方法之一则不允许并行执行。
- 协同程序，但它们也会泄漏出函数。
- Actor模型，但后期的Actor可以比较早期的Actor持续更长的时间，这意味着他们也可以泄漏出功能。
所以它们都会泄漏.
如果我只编写不会泄漏线程的函数会怎么样？
这就是解决方案：不要将线程从创建它们的函数中泄漏出去。
真的就这么简单。
这是 Nathaniel J. Smith想出来的，所以他称之为结构化并发，并撰写了 关于它是什么和为什么的开创性资料。
结构化并发可以传递一个一流的值（NJS 称之为托儿所，我称之为线程集）。
我后来意识到这也是一个问题；如果一个函数以某种方式返回一个线程集，就像一个异步函数返回一个future一样，那么里面的线程就会泄漏。
这就是为什么受限结构化并发（restricted structured concurrency：简称RSC）是缺失的部分：它让所有函数成为它们自己的子程序（具有并发性！），因此局部推理成立并且属性可以通过归纳证明。
受限结构化并发RSC 取消了将线程集作为一等值传递的能力。换句话说，RSC 是完全静态的，纯粹的编译时构造，并且它创建了一个线程树。
为什么析构函数必须运行
为了使受限结构化并发 RSC 正常工作，必须保证析构函数运行。
如果析构函数无法运行，则 RSC 可能会导致 use-after-free,，这是最严重的错误之一。
这也是线程集不能成为一流值，并且必须与特定上下文范围/生命周期绑定的另一个原因。
- 如果一种语言支持比 RSC 更多的并发原语（多线程 等并发概念），那么这很难做到，
- 但如果 RSC 是唯一的方法（没有线程等概念），那么实际上很容易保证析构函数运行：只需添加基于范围的资源管理（SBRM）。
那么，即使出现异常，析构函数也会始终运行。
我用 C 语言编写了一种SBRM 形式，并将我的所有线程集绑定到它。我甚至添加了setjmp异常longjmp和线程取消信号。
有了这些，只要我不在 SBRM 之外分配任何东西（，所有析构函数都会运行。而且是确定性的。
基于上下文范围的资源管理
一旦你有了 RSC 和是SBRM保证销毁，那么你就会解决两个重要问题： function colors 和异步清理问题。
- 如果每个函数调用都是其自己的子程序，那么您就没有函数颜色。
- 如果您没有异步，则无需担心异步清理。
这些问题在 Rust 中已经被认识到，有人说异步 Rust 根本不起作用，我同意这种观点。
Rust成功两个原因：
Rust 之所以受到人们的喜爱：
现在我们知道了为什么编写正确的程序很难：因为必须编写正确，但是，我们又无法始终验证所有程序。不过，没有什么可以阻止我们在某些时候验证某些程序的某些属性。
– Ron Pressler，“为什么编写正确的软件很难”
Rust 已经证明了编译器中的形式验证是 值得的。如果我们能以较少的成本增加更多功能，我们何乐而不为？
结构化并发RSC糟糕的地方
现在人们使用了几种并发代码模式，而 RSC 确实使它们更难实现：
- 生产者/消费者模式
- 线程池模式
需要同步是 RSC 的另一个缺点：
任何声音 API 最多只能提供以下三个理想属性中的两个：
- 并发：子任务与父任务同时进行。
- 可并行性：子任务可以与父任务并行进行。
- 借用：子任务可以从父任务借用数据，无需同步。
– without.boats，“范围任务三难困境”
再次重申一遍，runtime 比 comptime 更强大！
- 如果 RSC 只是一个 comptime（编译时期） 的东西，那么它就会一直受到痛苦的阻碍。
- 所以解决方案是使其动态化，拥有一些运行时runtime组件。
这就是催生了：动态受限结构化并发 (DRSC)
- 受限结构化并发RSC 取消了将线程集作为一等值传递的能力。换句话说，RSC 是完全静态的，纯粹的编译时构造，并且它创建了一个线程树。
- Matt Kline 可能正在考虑静态DAG；如果我们有 动态DAG 会怎么样？如果我们有动态 DAG 会怎样？如果我们不一次性（在编译时）生成线程和线程之间的边，而是允许自己动态（运行时）生成边，会怎么样？
DRSC 能够实现任何并发模式！
此时，阻碍我们接近 C10M 的唯一因素就纯粹是硬件了！
结论
如果我让 Rust 1.0 团队中的任何人相信 DRSC 的价值，那么他们现在一定很沮丧，这是因为 Rusty 的一些讽刺。
你看，Leakpocalypse 是由使用 Rust 所称的 thread::scoped() 时发现的一个设计错误造成的。本质上，这是结构化并发的早期形式！于是他们放弃了这个简单的解决方案！
如果他们那时推迟修补Bug，从设计上慢思考，做些困难的事情，推迟 Rust 1.0发布，完全真正解决这个问题，那么 Rust 可能会成为最优秀的超级语言！