Hacker News Reader

>but that's beside the point

It seems to me that it is an important point though.

> Even a non-constructive proof of existence for x can be significant in a programmatic context

Which has no relation whatsover to proofs and programms being the same thing.

A type-level program is still a program. Non-constructive proofs are addressing the question "will this program crash or go wrong if I extend it to do X, regardless of how I achieve that?", which is exactly the domain of type-level programming.

Programs and proofs are the same thing though according to the Curry Howard Correspondence, if I'm not wrong.

Reply on news.ycombinator.com