One thing that I really would like to impress upon computer people is that mathematics is not (usually) a formal computer language. Symbols and technical terms change meaning depending on the author, people write with different "accents". There's a little ambiguity and informality at times, but a whole lot less than other kinds of writing. Mathematics is (usually) written for humans, not computers. Don't attempt to r…
Why is that? Why is there not a universal way of writing mathematics that is not ambiguous and can be read by anyone that understands the 'language'? I have a deep dread and fear of numbers and mathematics in general because I don't understand them and I have never learned. Now I learn that there isn't one thing to learn but a vast array? No thanks. I had this apparently romantic view that an equation is an equation…
I think a more intuitive answer is that in math you are generally talking about relations between infinite sets of objects, whereas in programming you are living in a (in practice) finite space and are evaluating everything into an integer. Programming is about calculating integers, mathematics is about proving theorems. The language has to be very different because what is crucial about evaluating integers unambiguously is peripheral to proving theorems and vice versa.
You can ask, why is it so painful to give a formal proof of correctness of your program? It's impossible to do for all but the most trivial programs. You know that a brilliant person, given years of work, might be able to come up with a proof of correctness, but you also know that the language they would use to do that would be very different from the language that you as programmer would use to write your program. So it goes in both directions. Programs evaluate numbers, they are essentially adding machines, and central to that is the erasure of state via addition.
Math is about symbolic relations and erasure of state is via relations on infinite sets. For example, you want to prove that if a group has a prime number of elements, then it must be cyclic. So pick a generator, raise it to powers, and get a subgroup. Then by Cauchy's theorem, the order of the subgroup has to divide the order of the main group, and that order is prime, so therefore the subgroup has to be the whole group.
There are many things to unpack in that statement. For example, Cauchy's theorem, which says that if a A is a subgroup of B, then the order of A divides the order of B. So
Cauchy's theorem + Group is prime order => non-zero subgroups must be the whole group.
And then every non-zero group has a non-trivial cyclic subgroup + non-zero subgroups must be the whole group => the whole group is a cyclic group.
So it's bit like adding numbers, in that you forget state, but the rules are much more complicated involving quantifiers and a huge universe of sets.
To build a computer that could reason that way, you'd need an infinite set of registers, rules for quantifiers, etc. and your unit of memory would be abstract set relations instead of a zero or 1.
You can try to simulate special cases of that in software, say with an SMT solver. If you look at the DSL of writing code for SMT solvers, it looks different from the code that a programmer is used to writing, and the best SMT solver can't really do anything too interesting from a math point of view, with very rare exceptions.
Moreover in math as practiced, no one (except some logicians) writes in formal logic. It would be too cumbersome. Simple statements like "a harmonic function on a disk achieves its maximum and minimum value on the boundary of its domain" would require thousands of pages of formal symbols and quantifiers. No one can think like that, and so we don't write math that way because we also want to forget things and make compact statements, but what we forget in math is relationships among infinite sets, things like, what are the real numbers, what is a function on the real numbers, what is a differential, what is a harmonic function, what is the maximum of a function, what is a disk, all of that is packed into our statement and replaced with a math statement that is much more compact in the same way that 1 && 0 are replaced by 0 in a computer register, but the computer register is not rich enough to model relations on sets.