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

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.