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

[Sandro Magi]

(my first reply seems to have vanished into the aether, so apologies if
this gets posted twice)

Mathieu Suen wrote:
> On Dec 12, 2007, at 10:35 PM, Ben Laurie wrote:
>
>> One obvious reason to prefer static typing is that violations are
>> detected at compile time.
>>
>
> What kind of violation?
>
> For me it seem that most kind of violation that static type detect at
> compile time is also detect when you test you software with
> dynamically type language.
>

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.

James A. Donald wrote:
> The compiler is often running on someone else's machine,
> while the interpreter is running on your machine.  This
> seems like a reason for preferring run time typing for
> reasons of security, though it is often unacceptably
> costly in performance.

Type checking someone else's code is not costly, given that the code is
in a checkable format, ie. a bytecode. The more elaborate the code
format, the more powerful the type system needed to verify the
properties, ie. typed assembly languages and proof carrying code (PCC)
for assembly.

Still, checking a proof in PCC is not costly when compared to generating it.

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?

Sandro

[1] "Type Systems for Concurrent Processes: From Deadlock-Freedom to
Livelock-Freedom, Time-Boundedness.",
http://www.kb.ecei.tohoku.ac.jp/~koba/papers/IC-lockfreedom.ps.gz