The proofs/programs (Howard/Curry) correspondance has been fairly well established I think.

It's the requirements discovery phase that always breaks every pure mathematical treatment of software development.

(And also, like DW points, that software is way more complex. But on this case, it's the requirements discovery.)

That’s because it’s not pure math, but applied math. Which also has the requirements discovery phase.

Yes, and constructing mathematical theories is completely different from finding proofs.

It is a bit like architecture is just physics or painting is just chemistry. Technically true in some reductionist sense, but not necessarily the most useful way to think about it.

No, the premise is that programming is the act of writing precise specifications, which is easier in a precise language. Similarly to mathematical proofs.