[PRL] A type-based solution to the "strings problem":

[William D Clinger]

Matthis wrote:
>  HUH?

Cormac proposed a world-wide data base of witnesses to 
subtyping failures, to be extracted automatically from
application data that fail a run-time type check.  The
security implications should be obvious.

This isn't an essential part of Cormac's system, but
the fact he suggested it at all may indicate how much
thought he has given to the problem of refuting subtyping
assertions at compile time.

If subtyping assertions are not refuted at compile time,
then his system amounts to run-time checking with some
attempt to optimize away some of those checks at compile
time.  As for the string problem described in the article
Mitch cited, the essence of the problem is that programmers
cannot be relied upon to include those run-time checks in
their programs.  Cormac's system does not address that,
except by providing an alternative syntax for the assertions
programmers are using now.

Will