3 ms·
That is misleading. Simplifying a great deal, the Curry-Howard correspondence asserts the following identities between intuitionistic logic and pure functional
by YorkshireSeason 7y ago
That is misleading. Simplifying a great deal, the Curry-Howard correspondence asserts the following identities between intuitionistic logic and pure functional programming:
* Types = formulae
* Programs = proofs
* Beta-reduction = cut-elimination
Checking whether a string is a proof in a given logic is a simple computation.
- lostmsu 7y agoJust an addition to this comment: Point is that, according to Curry-Howard, validating a proof is equivalent to type checking the program, not actually running it to halting. Type checking (<-> validating a proof) is polynomial.