[E-Lang] Reliance & Static Security Checking

Bill Frantz frantz@communities.com
Thu, 04 Jan 2001 18:15:31 -0800

At 04:47 PM 1/4/01 -0800, Chip Morningstar wrote:
>MarkM says:
>>"rely" doesn't imply "reliable"; far from it.  That's why we conjugate it
>>"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
>>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
>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
>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
>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
>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.

There is a limit to what the compiler can do.  I can imagine stack and
queue objects, each of which implement only push and pop methods.  The
compiler might very well say they are the same interface, not being able to
read the differences described only in the comments.  I expect programmers
will not consider them to be interchangeable.

>Looking at our current set of issues from a compiler-centric perspective,
>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
>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
>the implementation matches the interface according to the rules I expect" and
>"suspect" means "not so assumed". Capturing this uncertainty is a worthy
>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
>to express what is known and now using it also to express what is unknown.
>like going from reasoning about systems of equations to reasoning about
>of inequalities: you may be in a world with the same basic formalisms as
>but suddenly everything got harder to think about.
>Is it any wonder that we are tending to get a little confused at times?

Now I am really confused.  Let me try to illustrate what I think MarkM is
trying to get at with an example.  Take a hashtable object (like the
java.util.Hashtable).  It has operations:

def hashtable {
  to put (:any key, :any value) :void { ... }
  to get(:any key) :any { ... }
  to delete(:any key) :any { ... }

The hashtable can be written so it does not rely on (is not at the mercy
of) the value object.  That object reference is merely saved and returned,
it is not invoked.  The hashtable does rely on (is at the mercy of) the key
object.  The hash table is going to depend on the key providing a stable
hashcode, and an equals operation which has certain characteristics (e.g.
commutativity and stability over time).

The :any auditor can not check these characteristics.  I also believe that,
in general, no automatic system can check them.  This makes the
rely/suspect pair very much like the /*null OK*/ comment convention adopted
by Java programmers to document whether a parameter/return value could be
null.  MarkM is suggesting some automatic checking on the part of the
compiler to warn about certain assignments.