[cap-talk] Type systems

[Mark Miller]

On Dec 12, 2007 5:26 PM, David Hopwood
<david.hopwood at industrial-designers.co.uk> wrote:
> The issue is, what does the "dynamically typed" language do when it sees a
> run-time type error (usually, it throws an exception), and can a security
> failure still occur if it does that (yes, if some object is an inconsistent
> state at that point, and remains accessible afterward).
>
> If there is any plausible case where a security failure could occur in a
> language that does not perform a particular check statically, that would
> have been prevented by performing it statically, then we can't claim that
> the language has provided *exactly* as much integrity.

Agreed. I'll make the weaker claim that with an Erlang-style "I
destroy my own vat anytime I suspect I might be inconsistent" policy,
then the language provides almost as much integrity. The remaining
inconsistency difference is in the recovery behavior of the vats left
standing.

E's provides less confidence that consistency is maintained, since
type errors are thrown rather than killing their vat. IIUC, E with
your backtracking proposal would indeed provide *exactly* as much
integrity as a statically typed language. So, ironically, my original
claim may be rescued by your future work. ;).

-- 
Text by me above is hereby placed in the public domain

    Cheers,
    --MarkM