[Haskell-cafe] Very freaky

[Neil Davies]

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 <andrewcoppin at btinternet.com> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>