[User23]

> language in maths is not a programming language used to tell a computer how to go from A to B, but a natural language

Right, we're on the same page, I just think this is a bad thing and you evidently think it's a good thing. I'm well aware many mathematicians don't, because it's how they were trained and unlearning is the hardest kind of learning. The ambiguity[1] of natural language is observably ill-suited for formal reasoning, and the experience of computing science has shown this conclusively.

Do bear in mind that the pioneers in our field were virtually all trained mathematicians. They were well aware of the historic faults of the field because having to make programs actually work forced them to be.

The legacy fuzzy pencil and paper approach of traditional mathematics is going to end up being to proper formal mathematics just as what's now called philosophy is to formal logic.

[1] Let's not confuse ambiguity with generality.