I find typing rules in theoretical computer science hard to read, and I just realized that it’s for a completely trivial reason: I subconsiously read “:” as having lower precedence than ⊨ and “,”, which is completely wrong, so I have to concentrate to group everything the right way.
The only reason I can think of for this is that way back when I learned Pascal, which allows declarations like “ x, y : integer”, which is somewhat like “:” being higher precedence than “:”.
I have a similar problem with geometric algebra (and I suspect other Clifford Algebras as well). The geometric product of a and b is written as ab. It is not, generally, commutative, and so can be broken down into a commutative dot product a?b and an anti-commutative wedge product a^b (so ab = a?b + a^b, a?b = b?a, a^b=-b^a). By convention, the geometric product has a lower precedence than the dot and wedge products. So ab^c should be read a(b^c) and a?bc should be read (a?b)c.
That simply looks wrong to me, ab looks more tightly bound that a^b or a?b. It’s gotten in my way of reading standard identities and understanding them.