Thanks so much for this introduction! For anyone interested, here is a link to Lamport's video introduction to TLA+, which I found really helpful and interesting http://lamport.azurewebsites.net/video/videos.html
It seems odd that the math is defined in such detail when this isn't supposed to be a tutorial or a reference. The emphasis on justifying and motivating TLA+ as a practical thing to learn suddenly disappears, and it's just one definition after another.
(It's also unclear to me whether these definitions are actually TLA+, since it's using non-ascii symbols. How esoteric is this language?)
> It seems odd that the math is defined in such detail when this isn't supposed to be a tutorial or a reference. The emphasis on justifying and motivating TLA+ as a practical thing to learn suddenly disappears, and it's just one definition after another.
My goal isn't to justify TLA+ as a practical thing to learn. The articles and tutorials I linked to in part 1 already do an excellent job at that. My goal is to do a deep-dive into the mathematical theory of TLA+, intended either for those who already know TLA+ or those who are interested in the theory of formal methods and formal mathematics. A little like how som Haskell programmers want to learn category theory.
> It's also unclear to me whether these definitions are actually TLA+, since it's using non-ascii symbols.
Yes, it's actual pretty-printed TLA+ code. You type it using ASCII symbols (`==` for `≜`, /\ for ∧, `~` for `¬`, `\in` for `∈`, `\A` for `∀`, `\E` for `∃`, `[]` for `◻` etc). In the IDE you edit in ASCII and can view the pretty-printed version. There's work on displaying in Unicode as you type.
> How esoteric is this language?
It's not as popular as Java or Python, but it's more popular than Coq. Amazon uses TLA+ to specify and verify most of AWS, Oracle and Microsoft do the same for some of their cloud services, and if you head over to https://www.reddit.com/r/tlaplus/ you can see other uses.
