Hacker News new | ask | show | jobs
by joel_ms 2773 days ago
How so? I've always felt that intuitionism/constructivism were closer to theoretical computer science due to constructivism requiring you to produce (or compute) the what you're trying to prove.
1 comments

Dijkstra and Scholten's https://www.amazon.com/Predicate-Calculus-Semantics-Monograp... is a good example of what I mean.

The state space is far too large to show a program is correct by constructing all possible processes it could execute. Instead you must show that the program admits no incorrect processes whatsoever, and as far as I know mathematical formalism is the only possible way to do that.

Of course if one just wants to make money, formal correctness is observably of absolutely no importance. And there's nothing wrong with wanting to make money!

From Wikipedia: > Brouwer the intuitionist in particular objected to the use of the Law of Excluded Middle over infinite sets

It always seems to me that using the LEM over infinite sets is akin to claiming that all problems are decidable.