News for hackers. Stuff that matters.

A comment on This is what is wrong with contemporary mathematics.

Re:This is what is wrong with contemporary mathematics by mshang on Saturday December 22, 2012 @01:37AM (#4955981)
> 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.

[ Parent | on HN ]
Re:This is what is wrong with contemporary mathematics by eriksank on Saturday December 22, 2012 @03:12AM (#4956121)
The 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.
[ Parent | on HN ]