[POPLmark] Experience report with Twelf

[Karl Crary]

I don't think I'm confusing anything.  My point is that the excluded 
middle arises solely because the operational semantics is required, 
primitively, to decide a question that formally is not known to be 
decidable.

I wouldn't really call the language safe if you can't execute it, but 
it's not my point to argue about the terminology.  If "unsafe" is too 
loaded of a term, shall we settle for a simpler term, such as "broken"?  :-)

    -- Karl


Benjamin Pierce wrote:

> 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
>
>
>