[E-Lang] Reliance & Static Security Checking

Chip Morningstar chip@groucho.communities.com
Thu, 4 Jan 2001 16:47:55 -0800 (PST)


MarkM says:
>"rely" doesn't imply "reliable"; far from it.  That's why we conjugate it to 
>"reliance" rather than "reliable".  "A relies on B" means "A's correctness 
>depends on B's correctness", or, equivalently, "A's correctness is at the 
>mercy of B's misbehavior".  Notably, it does *not* imply that A's programmer 
>believes B to be correct, just that A's programmer is willing to let A's 
>correctness be contingent on B's.  If "rely implies reliable" is too easy a 
>mistake to make, then we need to find yet another term.

If it were not too verbose, I'd suggest replacing "rely" with "vulnerableTo"
and "suspect" with "imperviousTo".  But it *is* too verbose :-)

One source of ambiguity here is between (Sense #1) reliance on an object's
abstract declared interface (its contract) and (Sense #2) reliance on its
implementation of that interface.

In the case of Sense #1, I am concerned with my own correctness: for an object
I am using, I want to be sure that the object's interface presents the
operations I'm intending to use and that I'm using them in a manner consistent
with the way they are described; for an object I am implementing, I want to be
sure that what I have coded matches what I'm telling other people about it.

In the case of Sense #2, I am concerned with the other guy's correctness: did
he actually do what he said he was going to do?

Both of these ideas can be captured in type declaration syntax, but programmers
historically have relied (there's that word again) on the compiler to handle
type declarations according to Sense #1 (in some cases, actually to generate
the implementation *from* the declaration). Thus the syntax only really had to
be able to express the programmer's own intentions. Responsibility for
certifying correct correspondence between the interface contract and the
implementation belonged to the compiler. Even when interface declarations were
used to express pledges from one programmer to another about what a program was
supposed to do, this was in the context of the compiler being the neutral
arbiter: those declarations mean the same thing to the compiler regardless of
which programmer presents them to it.

Looking at our current set of issues from a compiler-centric perspective, what
we are doing is introducing the complication that I don't have any way to be
sure that the other guy's compiler will certify the correspondence between the
contract and his implementation according to the same rules that mine
would. His compiler may be his Personal Tool For Evil or it may just be from a
different vendor who interpreted the language spec slightly differently.

Now what we are trying to do is extend the type declaration syntax to allow us
to make this uncertainty explicit.  MarkM's "rely" means "assumed a priori that
the implementation matches the interface according to the rules I expect" and
"suspect" means "not so assumed". Capturing this uncertainty is a worthy goal;
the concern I have is that it tends to undermine its own objective. The idea,
as with most data type formalisms, is to make it easier to reason about types
by enabling us to be explicit about previously unstated assumptions. However, I
think dealing with this trust issue in this fashion actually makes reasoning
more difficult.  You are taking a notation that people are accustomed to using
to express what is known and now using it also to express what is unknown. It's
like going from reasoning about systems of equations to reasoning about systems
of inequalities: you may be in a world with the same basic formalisms as before
but suddenly everything got harder to think about.

Is it any wonder that we are tending to get a little confused at times?