TLA+ 学习路线

TLA+ 是一种用于建模程序和系统的高级语言，特别适合并发和分布式的系统。

这种语言不是某种锦上添花、可有可无的技术，它是那种有需求的人绕不开、没需求的人一万年也用不到的技术。所以我不会在这里介绍 TLA+ 语言的基本概念，浅尝辄止的知识对于看到这篇介绍的大部分人都没有任何意义。

以下三步是我认为合适的学习路线，希望能让初学者少走一些弯路。

第一步，走完 learntla 教程：

https://learntla.com/introduction/

learntla 教程会让你了解大部分语法，懂得编写 TLA+ 和 PlusCal 规约，最好把环境搭建起来，自己跟着示例手动写一遍，在动手抄的过程中容易理解语法与效果。

第二步，把《用 TLA+ 定义系统》这本书看一遍，中文版是机械工业出版社的，英文版在官方网站上可以下载。

https://lamport.azurewebsites.net/tla/book.html

读完 Lamport 祖师爷的书，你会知道 TLA+ 的用法和含义。第 1 ~ 8 章是重点，需要读懂和掌握。其他部分高级主题可以跳过，比如第 9、10、11、19 章。

第三步，尝试自己编写规约，最好在已有示例的基础上，按自己的方式重构一遍，在重构过程中尝试添加新的东西。

网上总结的碎片式入门文章通常属于赛博垃圾食品，刚看完可能觉得很爽，但实际上远不如静下心学习，建议不要看。

挑选少数成体系的教程和书籍，配合动手实践，才是学习新领域的最好方式。