I agree!
Except that I think formal mathematics and proofs are attainable by informally-trained programmers... just perhaps not computer scientists.
To quote Friedrich Bauer:
"Software engineering is the part of computer science which is too difficult for the computer scientist."
I'm not sure how true that is. I don't have a computer science degree. I just have some interesting anecdotes from a colleague who is pursuing his Ph.D in computer science with a focus on developing a formal proof system. As a teachers' assistant he gets to run some classes. Most students tend to snore through formal methods I'm told. In order to wake them up he asked his students, who are working on their masters, to implement binary search. He gave them a specification for the algorithm and off they went in pairs. He used the PlusCal language from TLA+ to model around eight submissions in roughly two hours (I'm not sure what the exact number was). He found errors in 7 of them and was able to demonstrate what the inputs were and the steps the algorithm would take to reach the error state thanks to the model checker in the TLA+ toolbox. He got a few students hooked from that point.
In my case maths is exactly what I needed. I'd been working in distributed systems for years without an iota of training in formal methods. I'd read Leslie Lamport's papers on time, Paxos Made Simple, Raft, Bloom^L, etc. I have several common textbooks on distributed systems. I'd worked my way through many subjects in graph theory, "concrete" mathematics, discrete maths, etc. But as Nathan says what saved me most was experience and learning what abstractions to use and how to maintain a handle on complexity. If I just followed the code I could make things work. Except when the code wasn't a good enough abstraction (in the mathematical sense)... then things got hard (ie: race conditions, scheduling problems, etc). I used to just follow the code and suss out the problem using standard debugging tools and time-honored techniques but what started to really click for me was modelling my problem in TLA+. When I started leaning on maths I felt like I could start achieving more and solve problems before they became bigger problems.
I often talk about programming as a force-amplifier. If you're an actuary and you know how to program you will be a better actuary than your peers. Maths is the force-amplifier for programmers. You can learn formal mathematics and create a language for modelling computations that you can prove. Anything you can do from there will be better than what your peers can do.
... and yes I realize that not every piece of software needs to be accompanied by a proof. But for the hard problems it's a useful tool to have. And there are many other subjects where it's becoming necessary to understand different branches: graphics, AI, "big data" (ie: applied statistics), distributed systems (even your modern processor is a tiny distributed system), etc.