[POPLmark] Experience report with Twelf

[David Naumann]

I appreciate Benjamin's comment and am puzzled by the ensuing discussion. 
Karl (and Bob) have eloquently made the important point that doing a 
machine-checkable formalization can lead to design improvements in one's 
metatheory.  In theoretical work, separation of concerns is usually a 
design improvement, and that seems to be Benjamin's point.

On Tue, 30 Aug 2005, Benjamin Pierce wrote:

> Date: Tue, 30 Aug 2005 10:48:46 -0400
> From: Benjamin Pierce <bcpierce at cis.upenn.edu>
> To: Karl Crary <crary at cs.cmu.edu>
> Cc: poplmark at lists.seas.upenn.edu
> Subject: Re: [POPLmark] Experience report with Twelf
> 
> Hi Karl,
>
>> Type safety means that a well-typed program will execute successfully
>> until it terminates.  This means that if the program has not
>> terminated,
>> then a transitition exists and a machine can find it.  Usually the
>> specification of the operational semantics makes it obvious that a
>> machine can find whatever transition that exists, so we focus
>> exclusively on the former.  However, if the operational semantics
>> requires the machine to decide an undecidable problem, than that
>> language is *not* type safe.
>
> Seems to me this is confusing type safety with implementability.
>
> Suppose that the FJ subtyping relation were *not* decidable.   The
> evaluation of a program would still be perfectly determinate (since,
> mathematically, either S<T or S!<T for every S and T) , and one might
> still want to argue that this notion of evaluation was sound, in the
> sense that every well-typed term either is a value or is related, by
> the single-step evaluation relation, to some other well-typed term.
>
> Indeed, this would be exactly the case if we extended Fsub with some
> kind of downcasting.  Such an extension might or might not be a good
> idea, but I think it is muddling words to claim that it would be
> *unsafe*.
>
>       - Benjamin
>
>
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>