抽象是避免分心的有力工具。抽象一词的词源来自拉丁语，意思是“剪切”和“绘制”。通过抽象，您可以从复杂的系统中分离出协议，省略不必要的细节，并将复杂的系统简化为有用的模型。
例如，如果您对分布式系统的一致性模型感兴趣，则可以抽象出系统中的通信机制，因为这会造成不必要的干扰。
Leslie Lamport 在 2019 年的演讲中说：
抽象、抽象、抽象！这就是您赢得图灵奖的方式。
在亚马逊内部，抽象也非常有价值。我们看到熟练的工程师研究大型系统，切出协议/子系统，切入其本质，并深入进行更改以改进它或解决问题。抽象是一项无价的技能。这就是我标题中所说的“超越代码”的意思。
抽象 是一个非常有限的推理能够涵盖无数情况的唯一思维工具；因此，有效利用抽象能力必须被视为合格程序员最重要的活动之一。因此，有效利用抽象能力必须被视为一个称职的程序员最重要的活动之一。在这方面，我们不妨指出，抽象的目的不是含糊其辞，而是创造一个新的语义层次，在这个层次上，我们可以做到绝对精确。--埃兹格-W-迪克斯特拉
当我们说抽象时，我们不只是在谈论分层（如 OSI 模型）、接口或模块和封装。这是对抽象概念的狭义理解。更普遍的理解是细化：允许多种实现的高级抽象模型。
艺术在于看到/找到高层次的抽象模型，去掉不相关的部分，放大重要的部分。
您还需要弄清抽象组件的适当级别，以及该抽象组件的性质，以便在不干扰环境中其他子系统的情况下，实现您可能感兴趣的更高效或容错的实现。
抽象需要领域知识和适当的技能，以免抽象掉一个重要的细节/功能--在这里是指细节的第一层含义。
我们不能用产生问题的思维水平来解决问题--阿尔伯特-爱因斯坦
我们希望向新工程师传授这一技能。但我们该如何去做呢？我从 TLA+ 系列学习到的最大收获是：TLA+ 对于向工程师传授抽象艺术以及思考/推理分布式系统的正确方法非常有用。
别误会我的意思。我发现在我的系列课程中，抽象是最难教授的。要传达抽象概念，几乎需要潜移默化和某种禅意的传递。它在很大程度上仍然是一门艺术。
但 TLA+ 在传达抽象概念方面非常有用，下面我将尝试解释我为什么这么认为：
TLA+ 的基础：用数学进行指定
TLA+ 在分布式系统建模方面一直很受欢迎。Lamport 在 20 世纪 90 年代提出了它。由于 Lamport 与业界有着密切的合作关系，因此它建立在为实用系统建模的强大原则之上。
模型检查器出现于 2000 年。但即使在整个九十年代，TLA+ 也一直在为人们提供价值，帮助他们编写精确、明确的规范，并使他们专注于问题。
英语是模棱两可的。
使用数学而非编程语言进行规范有一种特殊的魔力。它迫使你关注 "是什么"，而不是 "怎么做"。它迫使你--震撼你--走出自己的舒适区。你必须进行数学思考。
经验丰富的开发人员很快就掌握了这一概念。我与团队中的七级和六级工程师一起工作，他们在几天内就能通过 TLA+ 提高工作效率。我编写了一个系统，而七级工程师放大了其中一个复杂的子系统，并在几天内编写了一个 TLA+ 模型。在另一个案例中，我建立了一个协议模型，而 L6 在几天内就掌握了 TLA+，并编写了协议的变体，用这些模型解决了他的问题。当我事后与他们交谈时，他们告诉我，他们希望所有的编程都能这么快。就像魔法一样。
TLA+ 的基础：全局状态转换模型
TLA+ 可以让您快速编写简洁的模型。马克-布鲁克（Marc Brooker）在公司的 Slack 上发表了一条随口评论，我很喜欢这条评论，并试着把它放到我所有关于 TLA+ 的演讲中。
全局共享内存模型肯定是一个方便的虚构--Marc Brooker
是的，TLA+ 通过协议动作为您提供了从一个全局状态到另一个全局状态的 "停止-世界 "转换，并为您提供了对您正在建模的分布式系统的全局状态的 "上帝视角"。其结果是，由于可以访问整个全局状态进行评估，因此安全不变性和有效性属性可以作为单线程编写。这种设置能让 TLA+ 用户以简洁、快速的方式对分布式系统进行建模和推理。
下面是 TLA+ 计算模型的简述。系统由两部分组成：
- 一组变量（全局共享内存模型）
- 一组赋值（称为 "actions操作"）
全局系统状态会随着动作将状态带入下一个状态，即 "状态"（如霍尔逻辑）而不断变化。
{state} 过渡-动作 {state'} |
最后，赋值的执行可以以谓词（即 guard）为真为条件。
以上就是全部内容。这就是 TLA+ 方便的虚构，它能让您快速编写简洁的模型。
TLA+ 迫使您进行数学/抽象思维
TLA+ 使您能够快速编写简洁的模型（通过为您提供全局共享内存这一方便的虚构工具）
我认为，这些都使得 TLA+ 成为探索设计空间、发现、改进或修复协议或协议变体的不可或缺的工具。
你可以从 AWS 的历史中看到这一利基。克里斯-纽科姆（Chris Newcombe）和蒂姆-拉夫特（Tim Raft）在 2012 年发表了亚马逊负责人演讲，让其他研究棘手的分布式系统协议的工程师注意到了 TLA+。他们在 2015 年发表了一篇论文，并与公众分享。这激发了业界对 TLA+ 的兴趣。
如今，AWS 中有数百种 TLA+ 模型，包括 S3、DynamoDB、EBS、EFS、Lambda、Journal 等。所有这些模型的共同模式都是有机的、草根式的参与，而不是通过规定或系统化的流程。
工程师面临着棘手的并发/分布式系统问题，他们头痛欲裂。然后他们意识到，他们需要在产生问题的更高层次上解决这个问题。他们通过口耳相传了解到 TLA+，并将其应用到他们的问题中，最终解决了问题。
然后，他们又离开去做其他事情，一做就是几年，直到他们看到另一个合适的问题来应用它。
这就是我教授迷你课程和录制讲座的原因。我喜欢教工程师们做好准备，这样当他们遇到问题时，就能从 TLA+ 建模中受益。
我之前提到的 L6 正在处理的问题是二级索引构建。这是一项后台工作。我的意思是，你不会认为这是一个并发/协调密集型任务，它就是一个后台工作。但它与前台操作之间存在着有趣而棘手的并发竞赛条件，使用 TLA+ 建模让它受益匪浅。如果您提前学习了 TLA+，您就会处于一个有利的位置（幸运会眷顾有准备的人），能够识别出何时这是一个可以应用 TLA+ 并从中获益的有用问题。