5 ms·
It is worth noting that according to the Curry-Howard isomorphism[0], programs are equivalent to proofs and vice versa. 0.https://en.wikipedia.org/wiki/Curry%E
by KhalilK 12y ago
It is worth noting that according to the Curry-Howard isomorphism[0], programs are equivalent to proofs and vice versa.
0.https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- wolfgke 12y agoYou have to pay close attention what system of logic the proofs are written in. So, for example, it is an open problem, how and whether proofs written in homotopy type theory can be interpreted computationally (source: http://en.wikipedia.org/wiki/Homotopy_type_theory#Computer_programming http://en.wikipedia.org/wiki/Homotopy_type_theory#Computer_p...).
- kmicklas 12y agoI thought this was more or less solved with the recent developments on the cubical sets models? There is even a toy interpreter with univalence and higher inductives: https://github.com/simhu/cubical https://github.com/simhu/cubical
- jonsterling 12y agoThey've done a lot of good work, but it's not quite done yet. The original conjecture has not been answered in the affirmative, and there are also further questions...