[cap-talk] David Wagner's Google techtalk is now up!

[Mark Miller]

> There are many, many program properties that a type system can prove
> that are absolutely impossible to test for. Deadlock freedom for
> instance [1]. Even various security properties can be proven by a type
> system, properties which cannot be extracted by testing unless the tests
> cover all possible program inputs, which is completely infeasible for
> any non-trivial programs.
>
> That said, Java has a fairly weak type system which can't even enforce
> properties achievable with capabilities.

I'd like to distinguish between systems that check that *type safety*,
as conventionally understood, is not violated, vs systems that prove
more interesting properties of systems, like deadlock freedom; even if
these proof systems encode their propositions in an extended notion of
"type". I do understand that this line is squishy and can't be
formalized.

As an example, Java statically checks types. Joe-E's auditors
statically checks other properties that are indeed quite useful for
security, and does attach these checks to an extended notion of
"type". E's auditors do something similar, but less statically. I did
not mean my previous comments about type checking to include, e.g.,
such auditing systems.


> Mark Miller wrote:
> > A dynamic type system can provide exactly as much integrity (safety,
> > consistency) as a static type system. In both cases, integrity
> > violations are prevented -- whether statically or at runtime.
>
> What definition of safety are you using?

Consistency is preserved.

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

    Cheers,
    --MarkM