I means that you can view programming as constructing "witnesses" to "proofs" - programs becoming the (finite) steps that, when followed, construct a proof.
Intuitionism only allows you to make statements that can be proved directly - no "Reductio ad absurdum" only good, honest to goodness constructive computational steps - sounds like programming (and general engineering) to me. Powerful when you grasp it - which is why I've spent the last 15 or 20 years considering myself as an intuitionistic semantic philosopher - reasoning about the meaning of things by constructing their proofs - great way of taking ideas, refining them into an axiomatic system then going and making them work. Take it from me - it is a good approach it generates exploitable ideas that people fund that make people money! Neil On 10/07/07, Andrew Coppin <[EMAIL PROTECTED]> wrote:
Jonathan Cast wrote: > On Tuesday 10 July 2007, Andrew Coppin wrote: > >> OK, so technically it's got nothing to do with Haskell itself, but... >> > > Actually, it does > I rephrase: This isn't *specifically* unique to Haskell, as such. >> Now, Wikipedia seems to be suggesting something really remarkable. The >> text is very poorly worded and hard to comprehend, >> > > Nothing is ever absolutely so --- except the incomprehensibility of > Wikipedia's math articles. They're still better than MathWorld, though. > Ah, MathWorld... If you want to look up a formula or identity, it's practically guaranteed to be there. If you want to *learn* stuff... forget it! >> So is this all a huge coincidence? Or have I actually suceeded in >> comprehending Wikipedia? >> > > Yes, you have. In the (pure, non-recursive) typed lambda calculus, there is > an isomorphism between (intuitionistic) propositions and types, and between > (constructive) proofs and terms, such that a term exists with a given type > iff a (corresponding) (constructive) proof exists of the corresponding > (intuitionistic) theorem. This is called the Curry-Howard isomorphism, after > Haskell Curry (he whom our language is named for), and whatever computer > scientist independently re-discovered it due to not having figured out to > read the type theory literature before doing type theoretic research. > ...let us not even go into what constitutes "intuitionistic propositions" (hell, I can't even *pronounce* that!) or what a "constructive" proof is... > Once functional programming language designers realized that the > generalization of this to the fragments of intuitionistic logic with logical > connectives `and' (corresponds to products/record types) and `or' > (corresponds to sums/union types) holds, as well, the prejudice that > innovations in type systems should be driven by finding an isomorphism with > some fragment of intuitionistic logic set in, which gave us existential types > and rank-N types, btw. So this is really good research to be doing. > On the one hand, it feels exciting to be around a programming language where there are deep theoretical discoveries and new design territories to be explored. (Compared to Haskell, the whole C / C++ / Java / JavaScript / Delphi / VisualBasic / Perl / Python thing seems so boring.) On the other hand... WHAT THE HECK DOES ALL THAT TEXT *MEAN*?! >_< _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
