4 ms·
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 t
by kd0amg 7y ago
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.
- agentultra 7y agoI'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.