It depends what kind of math and what they're doing though. Systems like Coq give you much more trustable code to put in your system, and higher degrees of trust for clients. But systems like Idris actually let you write code and use the proof engine to write trustworthy code.
Most of that "math", from the perspective of a programmer, is a small subset of graph theory, formal logic, and category theory useful for proving relationships and reflexivity so that the machine can help you.
> Even unit tests which don't involve proofs can be a problem sometimes because they lock down API inputs and outputs.
This is a much bigger problem than "hand written mocks are bad" (which they are, I agree). But it's quite out of scope to complain that because API endpoints are often sloppily deployed without versioning or introspectability, that all formal methods are wrong.
What's more, and I really want to push this point so I'll emphasize it: quickly producing broken code helps almost no one. If you're an artist playing with making a synthesizer whine? Maybe okay. If you're writing software intended to face the world and do real work? We can't just keep pretending we're all smart enough to do this without mechanical aid; we're NOT smart enough to do this without mechanical aid anymore. Programs integrate too many libraries and APIs.
> I imagine that adding proofs as part of the unit test suite would further increase the productivity cost overhead by a massive factor.
With Idris, it makes it so the program can write code for you. I've been learning it over the last 2 weeks and I'm totally fascinated by how much drudgery it takes out of total programming.
> In software development, you should avoid treating the code like if it's special or perfect
This is precisely what formal methods do! You challenge every piece of code you can and say, "Prove to me that what you've written doesn't have an obvious flaw!" You rewrite until both the human and the proof engine cannot see anymore. It is not sacred at that point (no one believes this), but at least you've acknowledged that you can write errors and started to mitigate them.
> There are always downsides, and we're crazy to pretend that every fancy new methodology is a silver bullet.
Actually, the entire industry has started to demand that developers do a lot more computation on their ends to make better software. The "prove more of your program and write total code" is just one side of the "do more work on your end" school. Another is, "Your software is in fact the output of this algorithm training from a dataset on 4 GPUs." We probably need a similar step forward for APIs (where APIs are invalid & unusable without a spec that governs them).
It is a change, but most commercial software engineers are handling user data that can be leveraged in disastrous every day. As you say, we need the wisdom to realize that it's difficult to guess the use case or security impact of the code we write on a daily basis, and we need to start taking that fact seriously. These heady days of being able to deny responsibility and shove out any software we want without consequence need to end.