Hacker News Reader

Comment by hwayne | Hacker News Reader

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

    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.

View on HN

That 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.

out 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+

I found "Specifying Systems" by Lamport, and the examples it gives, to be an excellent introduction and a stricter companion to 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.

I agree, latexisms in TLA are on eye brow level of weirdness. Lesser punctuation syntax is always better.

Reply on news.ycombinator.com