Hacker News Reader

Is Curry-Howard interesting if you're not programming with advanced type systems? It's my understanding that writing a function that returns an integer (for example) corresponds to proving that an integer exists. Whoop-de-do? This would imply that unless you're constructing a sophisticated return type, you're not proving anything interesting.

> code designed to run on the human brain

So it's legacy code that runs on the oldest hardware that we have.. Plenty of people are interested in updating this code so that it runs on more modern platforms. Actually, this is my favorite way to drill into a piece of mathematics: port it to python.

That's not quite true. Curry-Howard only applies to constructivist mathematics, which is a very tiny subset of mathematics proper.

That is a much more complicated question than you make it sound: https://cstheory.stackexchange.com/q/5245/1802