Subject: Re: Who's running your business?
From: "Stephen J. Turnbull" <turnbull@sk.tsukuba.ac.jp>
Date: Wed, 31 May 2000 04:58:31 +0900 (JST)

>>>>> "Bernard" == Bernard Lang <Bernard.Lang@inria.fr> writes:

    Bernard> according to Curry and Howard, writing the proof, or
    Bernard> writing the code is essentially the same thing
    Bernard> (isomorphism). Hence same difficulty.

Ian's point (one of them) is that difficulty is not additive here,
because you must do the translation.

Furthermore, one imagines that code was invented because humans don't
do proofs as easily as they do code.  Isomorphic, sure, equally
difficult, wa-hey, big leap there.

    Bernard> And there are systems that allow codevelopement of both,
    Bernard> or translation from one into the other. Already used for
    Bernard> some real problems.

This is _very_ useful, as it makes difficulty subadditive for the
relevant domain.  How big is the domain of "real problems" for which
they are helpful?


-- 
University of Tsukuba                Tennodai 1-1-1 Tsukuba 305-8573 JAPAN
Institute of Policy and Planning Sciences       Tel/fax: +81 (298) 53-5091
_________________  _________________  _________________  _________________
What are those straight lines for?  "XEmacs rules."