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.