(1) Specifying Systems by Leslie Lamport (https://lamport.azurewebsites.net/tla/book.html)
This is the original TLA+ textbook (I myself learned from it) and is very thorough, but sometimes fails to differentiate between specs which are model-checkable and specs which are not. Since model-checking has become recognized as the main source of value from TLA+, this might frustrate readers who think "woah, TLA+ can do THAT!?!?" only to be disappointed. I still like it, though. You can get a free digital copy.
(2) The TLA+ Hyperbook by Leslie Lamport (https://lamport.azurewebsites.net/tla/hyperbook.html)
Unfinished and unlikely to ever be finished (Leslie has stopped working on it), serves as a good companion book to Specifying Systems. I believe this is the only resource for learning the formal proofs capability of TLA+, which I myself have not yet used.
(3) The TLA+ video course by Leslie Lamport (http://lamport.azurewebsites.net/video/videos.html)
Very goofy, very fun. When Leslie teaches courses to engineers in person, he uses these videos. They're effective.
(4) Learn TLA+ by Hillel Wayne (https://learntla.com/introduction/)
A free online resource for learning TLA+.
(5) Practical TLA+ by Hillel Wayne (https://www.apress.com/us/book/9781484238288)
I own this book, and it is a great introduction to PlusCal (a pseudocode-type language that transpiles to TLA+) and TLA+ in general. Highly recommend! Along with the video course, probably the ideal starting point these days.
Is PlusCal more a gentle gateway or properly useful in real-world applications?
I lean towards starting with Lamport's book over Wayne's, because the latter seems very PlusCal-centric (and the layout and typography don't appeal to me), but that may be a mistake.
I think Hillel has said people find PlusCal easier to understand off the bat, but I don't recall exactly where he said that. In the Amazon TLA+ whitepaper (https://lamport.azurewebsites.net/tla/formal-methods-amazon....) different engineers found TLA+ or PlusCal easier to learn.
That continues to be my experience. It varies both by engineer, and (as you point out) domain. Also, as I said in a sibling comment, it’s also important to think about what people want to read, because models are extremely useful formal documentation of protocols and interactions.
Source: I’m one of the authors of that Amazon paper.
Also, for me, TLA+ and PlusCal have huge value as documentation and communication tools. It’s not about whether I would prefer to read TLA+ or PlusCal, it’s about which my intended audience would prefer. Different situations lead to different choices.
Also, TLA+’s syntax is (in my entirely subjective opinion) needlessly weird, and makes the semantics somewhat less approachable.
For me it's the opposite. I find programming language (and PlusCal) syntax weird, though not needlessly so, as programming languages are necessarily extremely complex. TLA+ is the cleanest, simplest, most natural syntax I've yet seen for describing computations (and it is not surprising that research into "natural" programming for non-programmers in languages like Eve has ended up with something similar), and it's hard for me to imagine any other syntax with clearer semantics. But obviously this is a matter of personal taste.
I don't particularly like PlusCal (and I find TLA+ easier to understand), but I've used it for low-level concurrent algorithms.
_In my experience_, PlusCal is easier for the average engineer to start with, because it lets me decouple learning about behaviors, learning temporal logic, and learning basic predicate logic. It's also my experience that for many people, it's easier and faster to learn PlusCal and then TLA+ than to start with TLA+.
But PlusCal adds syntax and has its own quirks and logic. So if you are fine with TLA+, it's unnecessary overhead and can distract from the core ideas. Here's a quick test:
Op(x, y) ==
/\ x > y
/\ \E s \in S:
/\ x' = F(s)
/\ UNCHANGED y
We choose some element s out of the set S, but only if x > y. That element gets fed into a function whose output is the value of x in the next step. y stays unchanged.
If x <= y the whole clause doesn't apply.