Curry-Howard maps typical practical tasks on the programming side to completely useless make-work on the math side. Turning a customer's name and address into text to make a mailing label has to happen at some point, but you really don't need to go through all those steps to show that if customers exist, then strings exist.
Re:Think in Math, Write in Code
by agentultra on Thursday July 18, 2019 @04:48PM
(#20473788)
I'm talking about hard problems. A proof for such a program you suggest is trivial and probably not worth knowing. A program is a proof that there exists a type which satisfies a proposition. Not all propositions are interesting and neither are all programs.
I may be wrong but I believe the Curry-Howard correspondence disproves your claim. One can translate between the two and find that they are equivalent.
The difficulty is that some programming languages are hard to model mathematically due to the way they were designed and implemented. Some, like Idris or Agda, make it easy to see the correspondences. Others like C or Javascript are harder.
The key to solving hard problems is being able to think concretely in abstractions. The best language we have for abstraction is pure mathematics.