hwayne • 14 hours 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.

2
elcapitan • 9 hours ago

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.

bvrmn • 14 hours ago

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