Hacker News Reader

You are probably thinking of intuitionistic logic versus classical logic. In the former, the law of excluded middle is not built in.

View on HN

Yes that's the one. Thanks

If you have heard of the Curry-Howard equivalence, that programs and proofs are the same thing, the proofs in question are constructive, intuitionistic proofs.

Reply on news.ycombinator.com