[plt-scheme] Standard ML in PLT Scheme

Sam Tobin-Hochstadt wrote:
> I disagree.  In almost any case where a language that ensures some
> invariant is translated to a different language that doesn't ensure
> that invariant, dynamic checks are inserted instead.

To be a little more precise, you're talking about examples where a lower 
layer *relies* on invariants that it doesn't trust the higher layer to 
enforce. This might simply be due to the pragmatism of separate 
development (e.g. Linux can't developed with, say, GHC in mind), or it 
might be to reduce the TCB. But the point is that the lower layer only 
dynamically enforces the invariants that it relies on to run predictably 
(e.g. invalid memory access). It could care less about invariants that 
the language runtime relies on (e.g. message not understood).

The crux of this discussion is about trust. Tomi Neste was essentially 
asking: for the invariants of the PLT runtime system, are we willing to 
extend the TCB of mzscheme to allow trusted authors to turn off some of 
mzscheme's dynamic checks when they can ostensibly prove them unnecessary?

My vote, incidentally, is no. This seems like a can of worms that's not 
worth opening. OTOH, if the PLT authors had a research interest in 
proof-carrying code, then the author of a typed sublanguage wouldn't 
have to be trusted. But I don't know that anyone's interested in going 
that direction.

Dave