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
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