[POPLmark] Experience report with Twelf

[Benjamin Pierce]

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