While writing
a parsing tutorial for TLA+ I came across something weird. Per page 271 of Specifying Systems, the addition operator in TLA+ has precedence 10 and the subtraction operator has precedence 11. This means that the _expression_ a + b - c is parsed (a + (b - c)) instead of the usual PEMDAS-style ((a + b) - c) we learned in grade school. I looked in SANY and confirmed the relative precedence is there as well. Oddly, multiplication and division have the same precedence (although only multiplication is associative; a / b / c will be a parse error).
Does anybody know why this design decision was made? Over fields like integers and reals a - b is the same as a + -b, so a + b - c becomes (a + (b + -c)), a kind of weird right-associative addition. Since addition is commutative over the integers and reals this should never matter (as in the final value of all ways of parsing the _expression_ should all be the same), but we can actually redefine addition and subtraction in TLA+ so it's possible they could be defined over a non-abelian group where this leads to unexpected behavior. I can't think of an example off the top of my head though.
Andrew Helwer