> Also, TLA+’s syntax is (in my entirely subjective opinion) needlessly weird, and makes the semantics somewhat less approachable. For me it's the opposite. I

> Also, TLA+’s syntax is (in my entirely subjective opinion) needlessly weird, and makes the semantics somewhat less approachable. For me it's the opposite. I find programming language (and PlusCal) syntax weird, though not needlessly so, as programming languages are necessarily extremely complex. TLA+ is the cleanest, simplest, most natural syntax I've yet seen for describing computations (and it is not surprising that research into "natural" programming for non-programmers in languages like Eve has ended up with something similar), and it's hard for me to imagine any other syntax with clearer semantics. But obviously this is a matter of personal taste. I don't particularly like PlusCal (and I find TLA+ easier to understand), but I've used it for low-level concurrent algorithms.