Interactive TLA+ - Jesse Davis and Samyukta Lanka
Channel: Markus Kuppe
Date: 2021-10-11

Learning TLA+ is a challenge for industrial programmers, who are accustomed to exploring their code’s behavior with a debugger and print statements, more than reasoning about it like mathematicians. Subtle mistakes in a specification can lead to a trivially-true specification. As Leslie Lamport says, “Always be suspicious of success.” Specifiers can catch such mistakes by exploring the spec’s behavior interactively, and they can gain a more intuitive understanding of TLA+.

This presentation is a survey of tools for interacting with TLA+, with guidance about which is best to use for which purpose. We will demonstrate:

* PrintT operator
* Error traces and trace expressions
* Graphviz output
* TLA+ Graph Explorer
* TSViz / ShiViz
* TLC REPL
* Debugger in TLA+ for Visual Studio Code

Finally, we’ll propose a vision for the future of interactive TLA+ spec development: which features are most important and how they can be consolidated into one tool.

Blog post: https://emptysqua.re/blog/interactive-tla-plus/