3 ms·
No, no, no. The Curry-Howard Isomorphism applies to functional programming languages only.
by jahewson 15y ago
No, no, no. The Curry-Howard Isomorphism applies to functional programming languages only.
- gatlin 15y agoAnd if those functional languages are Turing complete, then they are equivalent to all other Turing complete languages, and thus the C-H isomorphism would hold for all Turing complete languages.
- jahewson 15y agoNope. C-H concerns the simply typed lambda calculus which is not Turing-complete. Thus C-H only applies to non-recursive functional programs (or equivalent). A proof is a program, but a program is not always a proof (as proofs must terminate).
- gatlin 15y agoI concede. Thanks for the interesting tangent of reading that brought on, too!