3 ms·
> Mathematics and programming are not really all that related to each other I may be wrong but I believe the Curry-Howard correspondence disproves your claim.
by agentultra 7y ago
> Mathematics and programming are not really all that related to each other
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.
- kd0amg 7y agoCurry-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.
- deleted 7y ago[deleted]