[E-Lang] Reliance & Static Security Checking

[Mark S. Miller]

At 08:04 AM Tuesday 1/2/01, Karp, Alan wrote:
>I know even less about this topic than does MarkM.  However, my limited
>experience with provable correctness leaves me pessimistic of the prospects
>of using it in operational systems in the near future.  MarkM's proposal
>would seem to rely on this goal being achievable.  Never one to let
>ignorance stand in my way, I'd like to make a half-baked suggestion.

My intention was to only state goals that could be achieved by retargetting 
vanilla static type checking technology.  If anything in my proposal 
requires general program correctness proving ability, then I was very 
confused, as is certainly possible.  In any case, my intention is not to 
include any features that would require anything like that level of 
technology, even if we knew how to achieve it.  I believe in low hanging fruit.

The key is that "rely" is about the *unchecked* but assumed correctness of 
a component wrt its *not necessarily formalized* specification.  The static 
checking I'm advocating is about consistency among such reliance statements.


>There is one aspect that I think is immediately implementable, and he has
>given an example of it. [...]

This example is typical of the kind of static check I had in mind for this 
proposal to support.


        Cheers,
        --MarkM