One thing that bothered me while trying to learn the TLA+ is the two different but equivalent forms or syntax for writing it: a mathematical formula/expression form and code/program form. This topic is difficult as it, and having to deal with not one but two equivalent forms of saying one thing is perhaps a bit hard on a learner. I wish if there was a tutorial of TLA+ that ditched the whole mathematical formula notation, and taught only the code form.
They're equivalent in the sense that PlusCal, the pseudo-code-like language compiles to TLA+, the mathematical notation. The book Practical TLA+ teaches pretty much only PlusCal. Eventually, though, to get the full power, even those who start with PlusCal will need to learn at least some TLA+.
Comments
One thing that bothered me while trying to learn the TLA+ is the two different but equivalent forms or syntax for writing it: a mathematical formula/expression form and code/program form. This topic is difficult as it, and having to deal with not one but two equivalent forms of saying one thing is perhaps a bit hard on a learner. I wish if there was a tutorial of TLA+ that ditched the whole mathematical formula notation, and taught only the code form.
They're equivalent in the sense that PlusCal, the pseudo-code-like language compiles to TLA+, the mathematical notation. The book Practical TLA+ teaches pretty much only PlusCal. Eventually, though, to get the full power, even those who start with PlusCal will need to learn at least some TLA+.