>>Writing software is not math.
> You're wrong, and I've explained this upthread.
I suspect there is a difference in semantics, here. Software is inherently mathematical, yes. But the practice of writing software is not the practice of doing math.
The output of doing math is proofs. The output of writing software is...something that does something when run on a computer, hopefully interesting, meaningful, useful, or entertaining. In the vast majority of cases, we have not and will not need formal proofs of correctness for software to achieve these things.
If I want a blur effect on some portion of a UI, and choose to implement that with a Gaussian blur, what value is there in formally proving that a specifically Gaussian blur has been applied? All of this is inherently mathematical, but that doesn't imply a need for mathematical proof.