3 ms·
> Curry-Howard executable version of the claim I don't see how the code provided has any relation to the Curry-Howard correspondence, which is a statement rela
by mshang 14y ago
> Curry-Howard executable version of the claim
I don't see how the code provided has any relation to the Curry-Howard correspondence, which is a statement relating types and proofs.
- eriksank 14y agoThe original CH mapping, that is, "a proof is a program, the formula it proves is a type for the program" is quite hard to achieve because it tries to demonstrate that a particular statement is true. It is much easier to honestly fail in demonstrating that it is false.