> Truthfully, I'm somewhat baffled how it would ever even cross anyone's mind when designing a language to write type annotations like "x: X" given the long-established, pre-existing precedent in mathematics and the way its semantics seem backwards (if you had to use a labeling colon, "X: x" would make much more sense to me).

What maths precedent are you refering to? The thing I would consider most similar to today's type annotations are statements like "x ∈ ℝ" or "let x be a set of integers". In both cases the variable comes first.

Besides, it's much more practical this way. An identifier is very simple to parse and usually short, while types can be long monsters.