[POPLmark] Experience report with Twelf

[Steve Zdancewic]

Karl Crary wrote:
> 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"?  :-)

"Broken" As though that isn't loaded. :-)

I think Benjamin's point is that the definition of soundness makes no 
reference to the computability of the transition relation -- that is 
something that you're imposing on the definitions with the added 
condition that "a machine can find" the transition.  If I take the 
definition of soundness literally, I don't see any "machine" mentioned 
anywhere.

Soundness makes perfect sense for languages that can't be implemented on 
a Turing machine.  Whether or not such a thing is useful is another 
matter...

--Steve