[Flirts] RE: Curry-Howard isomorphism for Institutions

[Joseph Goguen]

Note: FLIRTS was down, but is now (said to be) up, so i am resending this.

Dear Valeria,

Thanks for the pointer to Phil's paper, i enjoyed reading it!

This paper does not make the claims for Curry-Howard that
you mention, but instead makes the much more modest claim
that systems were "designed by researchers in functional languages
and they depend heavily on logics and type systems whose roots
were traced in this paper" (these roots are work of Church,
Gentzen, Girard, etc.).  On the whole, there are pleasingly few
exaggerated claims in the paper.

My impression (e.g., looking at recent POPL proceedings) is
that there is indeed a lot of work that applies ideas from type
theory to programming languages, but the systems used are
far from beautiful, while the beautiful systems are not directly
useful.  It would be surprising to me if anyone worked out a
Curry-Howard isomorphism for any of these ugly type systems.

 - joseph

Valeria.dePaiva at parc.com wrote:

>Dear Joseph,
>
>While I do agree with 
>
>>The basic Curry-Howard isomorphism ("CHI") is one of the most beautiful
>>pieces of mathematics that is 
>>associated with computer science, and its extension to much more
>>general types is 
>>something that theoretical computer scientists can be proud of.
>
>I beg to differ on
> 
>>As far as practice goes, not much has happened,  
>>
>I guess it all depends on what kind of practice you're thinking of. It
>seems to me that quite a lot of the practical work that goes under the
>rubric of "programming languages" design&implementation (including the
>design of Java and other recent typed programming languages) owes its
>existence to programmers picking up the CHI and using it for their own
>purposes.  Phil Wadler had a nice note on Dr. Dobbs about the CHI called
>Proofs are Programs: 19th Century Logic and 21st Century Computing.
>
>I think the URL is
>
>http://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf
>
>But back to the subject at hand:
>
>>i even have some ideas which i hope to write up a bit later on.
>>Looking forward to seeing you this,
>
>Valeria
>
>-----Original Message-----
>From: Joseph Goguen [mailto:goguen at cs.ucsd.edu] 
>Sent: Friday, August 12, 2005 8:03 AM
>To: de Paiva, Valeria <Valeria.dePaiva at parc.com>; Formalism, Logic,
>Institution - Relating, Translating and Structuring
>Subject: Re: [Flirts] RE: Curry-Howard isomorphism for Institutions
>
>Dear Valeria,
>
>It seems to me that your definition of  "proof-theoretical" is too
>narrow to capture what mathematical logicians actually do; it seems to
>me that "proofs about proofs" is a more accurate definition for "proof
>theory", since in practice proofs about proofs are often done with
>respect to models, and experience shows that when you have the right
>models, such proofs are often easier that way.
>
>Im thinking that the origin of these divergences of view may go back to
>some discussions you and Till had about what's in the title of this
>thread, "Curry-Howard isomorphism for Institutions" and your research
>focus on type theory?
>
>The basic Curry-Howard isomorphism ("CHI") is one of the most beautiful
>pieces of mathematics that is associated with computer science, and its
>extension to much more general types is something that theoretical
>computer scientists can be proud of.  As far as practice goes, not much
>has happened, but it seems plausible to me that someday, for some class
>of useful programs, it may be possible for users to specify what they
>want in a "Visual Type Theory" language, which then an automatic theorem
>can constructively prove inhabited, yielding a program that can then be
>optimized by sophisticated transformations into a practical program that
>can be run.  After all, computers continue to follow Moore's law, which
>means still lots of power to come, while theorem proving and compiler
>optimization technologies continue to improve (but not exponentially!).
>So it seems worth continuing research on type theory in pursuit of the
>dream of automatic programming (and other some dreams).
>
>But i dont think this should be allowed to dictate the research
>programmes of institutions, which have always had different goals from
>type theory, one of which is to capture mathematical practice in logic,
>including model theoretic reasoning, not just formal manipulations of
>proofs.  Nevertheless, i think it could be very interesting to see what
>can be done with CHI in an institutional setting, and i even have some
>ideas which i hope to write up a bit later on.
>
>By the way, some time ago i put forward the slogan "types as theories"
>as a view of programming, and i also tried to show that if you have a
>nice module system of the sort supported by institutions, then you do
>not really need higher order logic to reason about typical higher order
>functions.  See
>
>    http://www.cs.ucsd.edu/~goguen/pps/utyop.pdf
>
>But this is not to say that i am against type theory or against higher
>order functions.  In fact, i endorse Till's proposal for research on IL,
>except that i do not think that the model aspect of morphisms should be
>optional.
>
>I look forward to further discussion of all this.
>
>  -- joseph
>
>Valeria.dePaiva at parc.com wrote:
>
>>Dear Joseph,
>>A small clarification:
>>
>>>im just reponding to your request for proof theory stuff that we can 
>>>do in insitutions - do you remember that request?
>>>
>>My request (may be I wasn't clear enough) was for proof-theoretical 
>>stuff that you could do with (the proof-theoretical side of)
>>"institutions with proofs".
>>
>>So Craig interpolation done by model theoretical means doesn't count, 
>>even if I do think it pretty. It's the `method' of proof that's at
>>stake in the request, not the statement itself.
>>
>>Cheers,
>>
>>Valeria
>>
>>-----Original Message-----
>>From: Joseph Goguen [mailto:goguen at cs.ucsd.edu]
>>Sent: Thursday, August 11, 2005 8:02 AM
>>To: de Paiva, Valeria <Valeria.dePaiva at parc.com>; Formalism, Logic, 
>>Institution - Relating, Translating and Structuring
>>Subject: Re: [Flirts] RE: Curry-Howard isomorphism for Institutions
>>
>>hi again Valeria!
>>
>>Valeria.dePaiva at parc.com wrote:
>>
>>>Craig interpolation I believe we can do totally proof-theoretically in
>>>many situations -- without infinite sets of sentences. Compactness, as I
>>>said, I have a problem  seeing it as proof theory, but maybe it's just
>>>lack of trying.
>>>
>>i never said craig interpolation needs infinite sets of sentences, and
>>i never said you couldnt do it proof theoretically!  im just reponding
>>to your request for proof theory stuff that we can do in insitutions -
>>do you remember that request?  and please note that compactness is
>>normally formulated as an assertion about proofs even though it is
>>normally proved model theoretically.
>>
>> - joseph
>>
>>>Best,
>>>Valeria
>>>-----Original Message-----
>>>From: flirts-bounces at informatik.uni-bremen.de
>>>[mailto:flirts-bounces at informatik.uni-bremen.de] On Behalf Of Joseph 
>>>Goguen
>>>Sent: Wednesday, August 10, 2005 6:25 PM
>>>To: Formalism, Logic, Institution - Relating, Translating and 
>>>Structuring
>>>Cc: till at informatik.uni-bremen.de
>>>Subject: Re: [Flirts] RE: Curry-Howard isomorphism for Institutions
>>>
>>>Dear Valeria and others,
>>>
>>>This is fun, we are getting a lot of different points of view.
>>>
>>>Valeria.dePaiva at parc.com wrote:
>>>
>>>>Dear Joseph,
>>>>Thanks for the friendly message.
>>>>First, let me make it clear that, no, I do not have "a nicer way of
>>>>>including proofs into institutions", at the moment. I had proposed to
>>>>>Till that we could investigate this problem together, as I had become
>>>>>interested in the idea around 1999. I'm attaching some slides from a
>>>>>talk I gave at NASA Ames then when I was trying to sell them a work
>>>>>proposal along these lines. I thought this was a cool idea, which you
>>>>>probably agree since you've had the same idea some 15 years before me.
>>>>>But I only worked on that for a couple of weeks, preparing the talk,
>>>>>which is just a proposal for some work. Not the work itself.
>>>>>
>>>>I'm afraid I don't think it excessive. I went back to the paper "What
>>>>is a Logic?" to see if I was forgetting any basic interesting 
>>>>proof-theoretic notion, given that you've said
>>>>>abstract way,     
>>>>>
>>>>But I don't see these many concepts. Would you like to discuss them
>>>>one by one?