对于许多软件工程师来说，设计是开发过程中不可或缺的一部分。就像建筑师绘制蓝图一样，程序员设计算法来支持他们的代码，并创建模型来设想他们系统的不同元素将如何协同工作。但是，如果程序员可以测试这些算法和模型以在它们变成编写代码中的错误之前发现设计缺陷呢？

这就是 TLA+ 的目标， TLA+是一种用于对软件程序和硬件系统进行建模的开源高级语言。其底层逻辑基于动作时序逻辑(TLA)，这是一种推理并发算法正确性的数学方法。TLA 和 TLA+ 均由Leslie Lamport开发，Leslie Lamport 是Microsoft Research的一位杰出科学家，他以发明LaTeX （一种用于科学论文的文档准备系统）而闻名。Lamport 还因其在阐明分布式系统行为方面的工作而获得了计算机协会颁发的2013 年 AM 图灵奖。

Lamport 很快注意到 TLA+ 不是一种编程语言，而是一种规范语言。“它在更高的抽象层次上描述程序——它应该做什么以及应该如何做，”他说。

这使得 TLA+ 对于验证程序的设计或支持算法是否有效很有价值，TLA+模型检查器使这一功能成为可能。在 TLA+ 上创建规范和编写模型后，工程师可以通过模型检查器运行所有内容，以在将设计错误实施到代码中之前发现并修复设计错误。

该语言首先在行业中用于为硬件建模，特别是在英特尔。“它最初对硬件工程师很有吸引力，因为 [他们] 习惯了在电路级之上精确描述事物的想法，”Lamport 说。“TLA+ 为他们提供了一种语言，他们可以用这种语言严格地表达他们的高级电路设计并进行检查。”

虽然它最初用于硬件领域，但 TLA+ 专门针对并发程序和分布式系统，强调正确性而不是速度。“这不是关于如何更快地计算某些东西，而是如何让进程相互交互，以便它们计算正确的东西，”Lamport 说。“随着系统变得越来越大，越来越多的工程师意识到让这些高级设计正确的重要性。”

当今的一些科技巨头已将 TLA+ 集成到他们的开发流程中。例如，亚马逊已经使用 TLA+ 来测试其云计算服务，并在其分布式系统中搜索难以发现但基本的算法缺陷，并在不牺牲正确性的情况下优化性能。微软在其Azure云计算平台上应用了类似的方法。Oracle的工程师在 TLA+ 的帮助下确保了他们的分布式系统设计是正确的。与此同时，开发欧洲航天局实时操作系统 Virtuoso 的小组Rosetta 宇宙飞船，在 TLA+ 上创建了下一个操作系统OpenComRTOS的模型。根据 Lamport 的说法，由此产生的代码库大约是其前身的十分之一。

然而，该语言不仅用于构建大型、复杂的系统。“如果您是编写一段并发代码的程序员，您可以针对该特定算法使用 TLA+ 以确保它是正确的并对其进行编码，”Lamport 说。

然而，挑战可以开始了。由于 TLA+ 是基于数学的，因此它具有困难的学习曲线，并且对软件工程师来说可能显得令人生畏。Lamport 创建了一些可以提供帮助的资源，但程序员可能会发现从PlusCal开始更容易，这是他为编写算法而开发的一种编程语言。PlusCal 算法的设计使其可以转换为 TLA+ 模型，然后可以使用模型检查器对其进行审查。

Lamport 已将维护 TLA+ 的责任转交给TLA+ 基金会，其创始成员包括亚马逊、Linux 基金会、微软和甲骨文。该基金会旨在“促进采用、提供教育和培训资源、资助研究、开发工具并建立 TLA+ 从业者社区”，以及“确保 TLA+ 语言的持续改进和发展”。

Lamport 认为，当前对该语言的最大需求是一种可以将高级 TLA+ 设计直接转化为代码的工具。但就目前而言，他希望这种语言能够帮助工程师进行软件或硬件开发的日常工作。“它改进了你设计系统的方式，”他说。“它让你跳出框框思考并改变你的思维方式。”