Gabriela Moreira，Quint 的 CEO 及 Informal Systems 的访谈系列

Gabriela Moreira，Quint 的 CEO 及 Informal Systems 的研究工程师，专注于编程语言和形式方法，致力于打造工具，使复杂系统的验证更容易被工程师所接受。她领导了 Quint 的开发，Quint 是一种基于 TLA+ 的现代可执行规范语言，她继续维护和演进该语言及其工具。她的工作涵盖正式验证、静态分析和开发者工具，她还通过教授形式方法为学术界做出了贡献，体现了实践工程和理论深度的融合。

Quint 由 Informal Systems 开发和维护，是一种现代的规范语言，旨在模拟、测试和验证复杂系统，如分布式网络、区块链和数据库。基于 Temporal Logic of Actions (TLA+) 的基础，Quint 引入了更易于开发者的语法，以及高级工具，如类型检查、模拟和模型检查，允许工程师在部署前检测系统故障。该平台强调可执行规范，允许开发者不仅描述系统行为，还可以积极测试和探索它，弥合了理论正确性和实际实现之间的差距。

让我们回到开始，你最初对编程的兴趣是什么？你是如何找到自己在形式方法和分布式系统中的位置的？

我是一个热衷的游戏玩家，拥有一个糟糕的电脑，我意识到我喜欢解决问题和让它正常工作。我报名参加了计算机科学课程，并被理论和编译器所吸引。

2015 年，我参加了编程比赛。在这些比赛中，你通常会得到一些输入和预期输出的例子，你需要编写代码来解决问题并使其适用于这些例子。然而，在提交代码进行评估后，代码实际上会被测试更多的例子，而这些例子超出了最初展示的范围。这种认识，即代码可能适用于我看到或思考的场景，但仍可能在我未考虑到的情况下失败，使编程成为了一种我爱上的挑战。

在行业工作中，我很快被分布式系统所吸引，我们需要考虑不同消息到达的顺序、不同故障模式和一系列隐藏的行为。2018 年，一位同事向我介绍了一种名为 TLA+ 的形式规范语言。我被深深吸引。从那时起，我开始围绕 TLA+ 构建工具，并一直在这个领域工作。

你围绕形式方法和编程语言构建了你的职业生涯，从早期基于 TLA+ 的工具工作到领导 Quint 在 Informal Systems 的开发。是什么激发了你专注于使形式验证更易于使用的动力？这种愿景如何塑造了 Quint 的设计？

TLA+ 太好了，不应该仅仅局限于少数人使用。我当时还很年轻，当我学习 TLA+ 时，我会加入同事的电话会议，尝试一起找到解决方案，但我经常发现自己是最后一道防线，抵御那些在大多数情况下会失败的场景。我认为必须有更好的、更有价值的方式来解决这些场景。因此，使用形式方法创建规范的想法在实施代码之前就诞生了。于是，我开始了我的学术旅程，这让我来到了 Informal Systems 和 Quint。

Quint 最初并不是作为一个产品而设计的。我们出于必要在 Informal Systems 中构建了它。我们为需要更多信任的系统编写了 TLA+ 规范，但由于语法太可怕，数学符号太多，工具也没有达到人们的基本期望，所以它并没有超出很小的一群人。我们会向同事和外部合作伙伴展示：“看这个令人惊奇的东西我做了”，但他们无法阅读它，也没有时间学习一种新工具。

Quint 的设计选择直接源自这种经历。该语言易于阅读和记忆。我们首先构建了一个 VSCode 扩展，能够在输入时突出显示错误。它具有类型和明确的模式来分离层次。它具有 REPL，让你可以交互式地探索它，还有一个模拟器，让你可以快速获得反馈并迭代。它将跟踪导出到标准化的 JSON 格式，易于机器解析。这些都是程序员已经期望从他们的工具中获得的东西，也是我们自己需要的东西。底层的验证逻辑与 TLA+ 相同。

对于不熟悉它的读者，你如何解释 Quint 是什么，以及为什么需要一种新的规范语言来与现有的工具如 TLA+ 一起使用？

大多数规范都是文档。你写下系统应该做什么，并通过阅读它们来检查它们。问题在于文档可能以机械检测无法发现的方式出错：未定义的名称、模糊的行为、隐含的假设。通常，你是在实施或生产过程中发现这些问题的。

Quint 规范是可执行的。你将系统建模为状态机，定义它应该满足的属性，并运行或验证模型。如果存在违规，你会得到一个反例，显示触发它的确切步骤序列。这改变了你捕获设计缺陷的时间和成本。

Quint 旨在弥合形式方法和日常软件工程之间的差距。与传统方法相比，你试图消除哪些最大的可用性障碍？

老实说，最大的可用性障碍是语法。这就是我们首先解决的。解决了语法问题后，我们可以专注于其他因素。Quint 的类型和效果系统可以标记出尽可能多的错误，然后再开始常规验证过程，人们非常重视这一点。类型几乎全部被推断出来，效果对用户是隐藏的，因此这增加了价值而没有任何摩擦。

Quint 的一个主要优势是其能够在部署之前对分布式系统进行建模和测试。这种功能如何改变工程师对构建诸如区块链或实时基础设施等系统的思考方式？

最大的转变是将验证提前。TLA+ 的创造者 Leslie Lamport 将编写规范与编写蓝图进行比较，即使你已经建造了某些东西，没有蓝图，也仍然有必要写下蓝图并用它来指导你的进一步修改。

Quint 建立在 TLA+ 的基础上，TLA+ 被广泛用于描述分布式系统。如何在保持理论严谨性的同时使语言更易于开发者使用？

关键的决定是限制 Quint 到 TLA 的一个片段，而不是暴露逻辑允许的所有内容。TLA 非常富有表现力，一些表现力包括工具不支持的运算符，并允许人们理解和错误使用的组合，使得调试非常困难。我们做出了一个刻意的选择：坚持大多数现实规范实际需要的东西，避免可能引起混淆的东西。

你还曾参与过静态分析和类型系统的工作。这些经历如何影响 Quint 的类型检查、工具和整体开发者体验？

我在那个世界中学到的最重要的教训是，并非所有语言都是一样的。你会听到人们说，这只是学习一种新语法，所有概念仍然相同，因此所有语言都是一样的，仅仅是个人喜好问题。这是不正确的。编程语言领域有伟大的研究人员，他们做出令人惊叹的工作来推进这个领域，这不仅仅是让语言看起来更漂亮或更符合他们的喜好。

作为讲师，你对工程师关于形式验证的最常见误解有何看法？

嗯，我教的是刚刚进入行业的本科生。他们中的大多数人以前从未听说过形式方法或形式验证，所以没有误解！课程安排得很好，大多数学生也没有学习分布式系统，甚至有一半的学生会在同一个学期学习线程。我告诉他们，我觉得自己像是在教他们什么是雨伞的用途，然而他们还没有经历过任何雨！

随着 AI 与软件开发的日益结合，你是否认为 AI 在帮助开发者使用 Quint 等工具编写、验证甚至生成形式规范方面有作用？

一个重大的作用，并且它已经在发生。计算机科学比编写代码更广泛，AI 为使用形式方法开启了完全新的方式。LLM 很擅长从自然语言描述的系统和现有代码中编写 Quint 规范，甚至可以产生可以立即运行和检查的 Quint 规范。

展望未来，形式方法需要发生什么变化才能从小众采用转变为软件开发生命周期的标准部分？

有一段时间，我知道 Quint 需要两件事才能获得更多采用：降低成本和提高价值。我认为这也适用于其他事情。形式方法刚刚在这两方面获得了巨大的提升，AI 大大降低了编写形式规范的成本，并创造了一个缺乏信任和理解的环境，在这种环境中，形式方法可以带来最大的影响和价值。

随着 AI 改变我们的职业，至少在某种程度上，我希望这种变化是朝着更高层次的设计选择和行为正确性发展，使形式方法成为日常工具；而不是我们不再理解任何代码或系统，并且花费所有时间审查 AI 生成的代码，而没有任何工具来帮助我们理解它。

感谢您这次富有洞察力的采访；对 Quint 感兴趣的读者可以通过 Quint 了解更多关于此可执行规范语言的信息，包括其工具和入门方法。