Factually accurate (to some degree), but almost completely irrelevant.
First, not all problems that can be solved with code are math problems. Take driving a serial port, for instance. There might be some aspects of it that are mathematical, but mostly it's a matter of interfacing with the chip spec.
Second, even for problems that are isomorphic to a math problem... the thing about isomorphisms is that they aren't identical. One form or the other is often easier to deal with. (That's one of the reasons we care about isomorphisms - we can turn hard problems into easier ones.)
Well, which is easier, writing programs or doing proofs? Almost always, writing programs is easier. This is why it's (almost) completely irrelevant.
Nobody wants to write code that way. So nobody cares. They're not going to care, either, no matter how forcefully you point out Curry-Howard.
Now, as you say elsewhere, you can gain insights from math that can change your code. That's true. But I suspect that most of the time, you don't actually write the code as a proof.
