在计算机科学领域，编程语言的灵活性与使用的安全性之间存在着一种持续的张力。程序员希望语言能够允许他们构建复杂的、动态的系统，让函数可以根据任务实时改变其行为，就像一把能根据任务调整工具的瑞士军刀。然而，这种灵活性往往是有代价的：程序在运行时实际会做什么，变得极其难以预测。它会完成任务吗？还是会陷入死循环？它会崩溃，还是会产生正确的结果？几十年来，研究人员开发了被称为“类型系统”的系统作为安全网，在代码运行前进行检查，以确保其遵循逻辑规则。在这些系统中，一种被称为“交集类型”（intersection typing）的方法已被证明在分析程序行为方面非常强大，但在应用于现代编程特性——即允许开发者拦截并管理意外事件（称为“效应”，effects）——时，这类方法在历史上一直面临困难。

本文介绍了一种看待这些安全检查的新方式，特别是针对处理此类事件的现代编程风格。研究人员 Stefano Catozi、Ugo Dal Lago 和 Taro Sekiyama 创建了一种全新的系统，该系统不仅可以追踪程序计算了什么，还可以精确追踪程序如何与周围世界进行交互。他们发现，通过将程序触发的事件序列视为其身份的核心部分，他们可以创建一个保证结构良好的程序一定会完成工作的系统。此外，他们发现通过简化这个复杂的系统，可以创造出一个不仅安全而且在数学上可预测的版本，从而允许计算机自动验证程序是否能达到特定目标。这项工作解决了一个长期存在的谜题，即为什么某些先进的编程特性会导致自动化验证变得不可能，并为构建更可靠的软件提供了一条清晰的路径。

要理解这个问题，首先必须了解现代程序如何处理“效应”。在传统计算中，程序通常被视为一个闭合的盒子，输入数据并产生输出。但在现实中，程序经常需要执行诸如读取文件、等待用户点击按钮或做出随机选择等操作。这些被称为“代数效应”（algebraic effects）。在旧系统中，这些效应的行为规则是硬编码在语言中的。在较新的系统中，程序员被赋予了定义自己规则的权力。他们可以编写一个“处理器”（handler）来拦截一个效应，决定如何处理它，然后继续程序运行。这功能极其强大，允许实现诸如撤销操作、模拟不同结果或管理复杂数据流等功能。然而，这种力量也带来了隐藏的危险：由于处理器可以以如此多的方式改变程序的流程，使用标准的数学工具来证明程序是否会停止运行，或者是否会达到预期状态，变得几乎不可能。先前的研究表明，对于这些先进系统，检查程序是否能达到特定结果的问题是“不可判定”的（undecidable），这意味着没有任何计算机算法能为所有可能的情况求解。

作者们致力于改变这一点。他们首先开发了一种新的类型系统，称之为 HEBI。简单来说，类型系统是一套规则，它为每一段代码分配一个标签，描述该代码被允许做什么。这里的创新在于，他们的标签是“行为性的”。系统不仅仅说“这个函数接收一个数字并返回一个数字”，而是描述了计算的整个故事。它记录了效应发生的顺序、传递给它们的数值，以及程序的未来如何依赖于这些效应的结果。想象一个程序询问用户的选择，并根据该选择执行两个不同的动作之一。新系统不仅记录了做出了选择，还绘制了整个可能的决策树，追踪程序可能采取的每一个分支。通过这样做，他们创建了一个足够精确的系统，能够捕捉程序的精确行为，包括它如何处理中断和恢复。

本文的第一个重大发现是，这个新系统具有极高的准确性。研究人员证明，如果一个程序可以在他们的系统中获得一个标签，那么它就保证能完成工作。反之，如果一个程序保证能完成工作，它总能被赋予一个标签。这是计算机科学中一种罕见且强大的属性，被称为“刻画终止性”（characterizing termination）。这意味着该系统能够完美地区分哪些程序会无限运行，哪些会停止。他们通过将一种经典的数学技术进行改进，使其适用于新的行为标签，从而证明了该系统足以处理处理器与其管理的效应之间的复杂交互。这证明了先前系统中问题的不可判定性并非编程风格本身的固有缺陷，而是用于分析它的工具的局限性。

然而，一个完美的系统往往过于复杂，以至于无法自动使用。研究人员知道，虽然 HEBI 可以描述任何终止程序，但其生成的可能标签数量之多，使得计算机无法在合理的时间内检查所有标签。这引导他们走向了第二个、或许更具实际意义的发现。他们问道：如果我们采用这个强大的系统，通过减少一些灵活性来简化它，使其更容易检查，会怎样呢？他们创建了一个更简单的版本，称为 HEB。在这个版本中，系统仍然追踪事件的顺序和处理器的行为，但它限制了程序分支展开的方式。它强制程序遵循一条更线性的路径，确保可能的变体数量保持有限。

这种简化的结果是一项突破。研究人员证明，对于这个更简单的系统，检查程序是否能达到特定结果的问题是“可判定的”（decidable）。这意味着计算机现在可以自动验证以这种风格编写的程序是否会达到期望状态。这与之前的情况相比是一个显著的转变，因为在之前的类似系统中，这种验证被认为是无法实现的。成功的关键在于意识到，他们原始系统的复杂行为性质可以作为这个更简单系统的“精化”（refinement）。他们展示了每一个符合 HEB 简单规则的程序，都可以映射到 HEBI 系统中一组特定的、有限的描述。因为这个集合是有限的，计算机可以通过穷举搜索来找到答案。

这项工作也阐明了旧系统为何失败。研究人员表明，先前方法中的不可判定性源于那些系统允许通过无限多种方式来精化程序的行为。在旧系统中，一个单一的类型可以扩展成无数种不同的变体，使得检查它们变得不可能。相比之下，他们的新系统施加了一种结构，使这些变体保持有限，同时保留了丰富的行为细节。这为理解从旧的、较简单的编程模型向新的、更强大的编程模型跃迁时的复杂度提供了清晰的解释，并提供了一种驯服这种复杂性的具体方法。

这项工作的意义不仅限于理论。它表明我们可以构建既高度灵活又经过严格验证的编程语言。通过使用捕捉事件序列的行为类型，开发者可以编写处理复杂现实世界交互的代码，而无需牺牲证明代码安全性的能力。研究人员不仅提出了一个新想法，还提供了一个完整的数学证明，证明了他们的系统在程序运行时能保持代码的安全性，并且可以用于自动验证可达性属性。这为未来开发更可靠的软件工具打开了大门，例如用于医疗设备、金融系统或自动驾驶汽车等对失败零容忍的系统。

最后，这篇论文关乎寻找平衡。它表明，处理程序中复杂、动态事件的能力并不一定非要以牺牲可预测性为代价。通过改变我们观察程序行为的方式——关注计算的故事而非仅仅是最终结果——研究人员在现代编程的灵活性与形式化验证的安全性之间架起了一座桥梁。他们证明了，借助正确的工具，我们可以理解并控制即使是最复杂的软件行为，从而确保我们的数字系统即使在变得更加复杂时依然保持可靠。这项工作证明了严谨的数学分析在解决计算机科学实际问题方面的力量，为下一代编程语言奠定了新的基础。