> I find one of the biggest mistakes programmers have about mathematical notation is that it's somehow just a terse, badly implemented programming language. But this is a very poor understanding of what mathematical notation is doing.
No, we think that because proofs and programs are isomorphic[1]. It's not a mistake: traditional mathematical notation provably is a terse badly implemented programming language. Actually it's worse than that, because oftentimes it doesn't even parse. Now I'm not going to say I can't on some level see the appeal. After all I think Perl is a lot of fun to code in.
Naturally, its adherents are practiced at making a virtue out of its defects. Who wants to admit they dedicated considerable brainpower to doing something in a fundamentally suboptimal way? That doesn't really matter though. As Mathematica and other tooling shows, the formalists have already won and now it's just a matter of mopping up the stragglers, or waiting for them to age out. This isn't terribly surprising to those who know the basics of the history of mathematics. It took something on the order of two centuries before Recorde's innovation of the equal sign was generally accepted.
[1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...