[E-Lang] Reliance & Static Security Checking
Mark S. Miller
Thu, 04 Jan 2001 12:55:49 -0800
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.