3 ms·
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
by billfruit 8y ago
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.
- pron 8y agoThey'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+.