share
Stack Overflow"A proof is a program; the formula it proves is a type for the program"
[+17] [0] Grigory Javadyan
[2011-06-01 16:23:19]
[ haskell ]
[ http://stackoverflow.com/questions/6204484] [DELETED]

This might be a philosophical kind of question, but I believe that there is an objective answer to it.

If you read the wikipedia article about Haskell, you can find the following:

The language is rooted in the observations of Haskell Curry and his intellectual descendants, that "a proof is a program; the formula it proves is a type for the program"

Now, what I'm asking is: doesn't this really apply to pretty much all the programming languages? What feature (or set of features) of Haskell makes it compliant with this statement? In other words, what are the noticeable ways in which this statement affected the design of the language?

(1) Anyone care to explain why the "close" votes, please? - Grigory Javadyan
I recall reading that H.C. quote in regards to Agda. Proof assistants like Agda and Coq are a slightly better embodiment of that statement than Haskell. - Dan
(1) @Grigory Javadyan: I didn't vote to close, but it's probably because the question is borderline off-topic for SO--philosophical questions, objectively answerable or otherwise, aren't generally appropriate here. In this case I think it's justifiable, though, because the answer has deep practical implications for how Haskell is actually used. - camccann
@camccann: I'd add that if you aren't immediately familiar with CH, then the question would seem much more unanswerable and possibly subjective than it actually is. - sclv
(1) @Grigory: if this question was a real problem with a real solution (in code) then it can stay on SO. Voted to close and move to Programmers. - sixlettervariables