想象一下，你正试图建造一座超级坚固的堡垒，来保护一座数字城堡。在计算机科学的世界里，这些堡垒被称为程序逻辑（program logics）。它们是一套严格的规则，数学家和程序员利用这些规则来证明一段软件永远不会崩溃、泄露秘密或做出任何奇怪的行为。

长期以来，建造这些堡垒就像是在手工雕刻每一块砖。如果你想添加一个新功能——比如一种处理掉电情况（崩溃恢复）的方法，或者与大洋彼岸的其他计算机通信（分布式系统）的方法——你必须从头开始。你需要一种完全不同于仅仅“使用”堡垒的特殊“筑砖”技能。这既困难又缓慢，而且你无法轻易地将旧堡垒中的砖块复用到新堡垒中。

核心理念：“效应处理器（Effect Handler）”工具包

这篇由 Zichen Zhang、Simon Oddershede Gregersen 和 Joseph Tassarotti 撰写的论文，提出了一种构建这些堡垒的新方法。与其手工雕刻砖块，不如使用一种叫做**效应处理器（effect handlers）**的神奇工具。

把效应处理器想象成一本可定制的游戏规则书。在标准视频游戏中，跳跃或射击的规则是硬编码在引擎里的。但有了效应处理器，游戏引擎会说：“我还不知道‘跳跃’意味着什么；我会等着有人来告诉我。”然后，程序员可以写一段小程序（一个处理器），规定：“好吧，当玩家尝试跳跃时，我会让他们漂浮一会儿。”

作者构建了一个名为 FicusLang 的微型空语言，它没有任何规则，除了这个“等待指令”的功能。然后，他们编写了处理器来创建用于以下方面的规则：

• 内存（Memory）： 程序如何记住事物（比如便利贴）。
• 并发线程（Concurrent Threads）： 程序如何同时做很多事情（比如厨师同时操纵多个锅具）。
• 崩溃（Crashes）： 当断电并重新来电时会发生什么。
• 分布式系统（Distributed Systems）： 计算机如何在不稳定的网络上相互通信。

神奇的技巧：层层构建

最酷的部分在于，他们不仅仅是制定了这些规则，还证明了它们。他们从空语言开始，编写了一个“内存”处理器，并使用名为 Ficus 的逻辑系统证明了他们的内存处理器运行正确。一旦这个被证明了，他们就可以利用这个“内存”处理器来构建一个“并发”处理器。

这就像盖房子。首先，你证明你的地基是稳固的。然后，你利用这个稳固的地基建造第一层。一旦第一层被证明是安全的，你就用它来建造第二层。因为他们以这种方式构建，所以可以轻松地混合和搭配功能。如果你想要一栋既有泳池又有车库的房子，你只需将“泳池处理器”和“车库处理器”组合在一起，而无需重建整个地基。

更强的规则与新花样

由于他们是从底层开始使用处理器构建这些规则，他们发现自己可以做出比以往方法更强的规则。

• “暂停”技巧： 在标准的并发编程中，计算机可以在任何微小的瞬间停止一个任务，以切换到另一个任务。这创造了难以追踪的巨大混乱。作者的处理器仅在特定的“效应”发生时（例如请求读取文件时）才会切换任务。他们证明了这种“仅在被要求时暂停”的方法与“随时暂停”的方法一样安全，但更容易进行推理。
• “水晶球”（预言变量/Prophecy Variables）： 有时，为了证明一个程序是安全的，你需要知道一个随机事件在发生之前会做什么。作者创建了一个“水晶球”效应处理器。它允许证明过程说：“我预测这个随机数会是 5”，然后在稍后检查是否正确。他们展示了如何从一个巨大的全局水晶球中构建局部水晶球（针对一个特定的变量），甚至可以让它们在进行内存操作时自动出现，而不需要程序员编写额外的代码。

“关系型”逻辑：双胞胎测试

该论文还引入了一个新工具，叫做 RelFicus。想象一下你有两对完全相同的双胞胎，程序 A 和 程序 B。你想证明如果给它们相同的输入，它们的行为总是一致的，即使其中一个版本与另一个版本略有不同。

RelFice 是一个逻辑，它允许你在脑海中（使用“幽灵状态”或想象中的资源）并行运行这两个程序，以证明它们是双胞胎。这对于证明他们新的“仅在被要求时暂停”的并发处理器确实是安全的至关重要。他们使用这个双胞胎测试来证明，增加额外的“暂停点”（抢占/preemption）不会改变程序的运行结果，这证明了他们更简单、更易用的模型的合理性。

他们没有做的事情（以及他们拒绝的内容）

了解这篇论文不是什么非常重要。

• 他们并不是在说旧有的构建逻辑的方法（“手工雕刻砖块”法）是没用的。他们只是在说这种方法难以复用，也难以在其之上进行构建。
• 他们拒绝了认为构建这些逻辑需要理解复杂的抽象数学结构（如前人工作中提到的“ITrees”）的观点。他们认为，由于其使用的是开发者已经熟悉的标准编程概念（处理器），因此这种方法更易于理解。
• 他们并不声称已经解决了计算机安全领域的所有问题。他们专门构建了用于内存、并发、崩溃和分布式系统的处理器，但也承认其他功能可能需要新的处理器。

他们有多确定？

作者们非常有信心，但他们的表达非常严谨。他们不仅仅是“建议”这可能行得通；他们证明了这一点。

• 他们使用一个名为 Rocq Prover 的工具（一个检查数学证明的计算机程序）编写了整个逻辑系统。
• 他们证明了一个称为**充分性（Adequacy）**的定理，该定理保证了如果他们的逻辑说一个程序是安全的，那么该程序在运行时确实不会卡死。
• 他们证明了他们新的并发模型与标准的、更复杂的模型是等价的。
• 他们展示了他们的“水晶球”（预言）功能是如何通过从全局版本中派生出来的，从而证明了数学逻辑是成立的。

总结

这篇论文就像是给了计算机科学家一套 乐高积木，而不是一堆湿粘土。以前，如果你想建造一种新型城堡，你必须自己调制粘土。现在，你拥有了预制的、经过测试的用于“内存”、“崩溃”和“网络”的砖块。你可以将它们拼装在一起，而数学会保证你的城堡不会倒塌。它让构建复杂的、安全的软件不再像是一个人的艺术创作项目，而更像是一个协作式的建筑工地，在这里每个人都可以重复使用最好的部分。