Disclaimer: I’m one of the authors of this paper.
One of the other authors (Chris) came up with the phrase “exhaustively testable pseudo-code”, and it’s something that I really hope gets picked up more broadly. The challenges with getting both engineers and managers engaged with formal methods is real, and explaining things in that way has been very helpful. It’s also worth mentioning that TLA+ is only one choice of tool, and while it’s one I really like, it’s not the best at everything. There’s a world of alternatives, and lots of active research going on. One good example is the recent link to a talk by Peter Alvaro that appeared recently here: https://www.youtube.com/watch?v=ggCffvKEJmQ
I’m very excited about tools like TLA+, because they let me augment the things that I’m good at as a human by taking advantage of the things that computers are good at. I’m fairly good at coming up with new algorithms, at understanding requirements, and at noticing common problems in multiple areas. I’m really bad at exhaustively searching entire state spaces of billions of states. Really bad. My computer is pretty damn good at searching state spaces. Together, we make a team that’s much stronger than either individual.
I thought this was easier to read than Lamports paper. I want to learn TLA+ to model check what I’m doing at work.
Lamport’s book about TLA+ “Specifying Systems” is very readable, and available for free online. If you’re just starting out, I’d encourage you to take his advice and only read the first hundred pages or so, and leave the second half of the book for later.