4 ms·
I taught a lot of people TLA+ and while there's definitely essential complexity, a nontrivial amount is just syntactic friction. Consider \A x \in set: x.i
by hwayne 1y ago
I taught a lot of people TLA+ and while there's definitely essential complexity, a nontrivial amount is just syntactic friction. Consider
\A x \in set: x.id /= 1 /\ ~x.active
vs
all x in set: x.id != 1 && !x.active
The latter has the same semantics but is much easier to read for the average developer, and more importantly is easier to type without syntax errors.
- bvrmn 1y agoI agree, latexisms in TLA are on eye brow level of weirdness. Lesser punctuation syntax is always better.
- deleted 1y ago[deleted]
- elcapitan 1y agoThat is literally what is holding me back every single time I get back to TLA+. I love your book and posts and always use it as reference to get back into it, but most of that "getting back" is just trying to remember all the minutia of the syntax. I wish there was simply a transpiler from some common syntax into TLA+. I don't even need Pluscal for the most part, and I'm fine with the concepts of temporal logic.
- infinitebit 1y agoout of curiosity, how did you get comfortable with temporal logic? i’ve had a hard time finding good resources aside from H. Wayne’s stuff on TLA+
- elcapitan 1y agoI found "Specifying Systems" by Lamport, and the examples it gives, to be an excellent introduction and a stricter companion to https://learntla.com https://learntla.com. It has some chapters that give very precise definitions of how things work in TLA (both on a language level as well as model checking), which answered some questions I often had along the way in more informal introductions.