[E-Lang] Reliance & Static Security Checking

[Mark S. Miller]

At 06:15 PM Thursday 1/4/01, Bill Frantz wrote:
>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.

An excellent example.  Stack and Queue may very well have the same 
signature, but they have different type *names*, which correspond to 
differently commented type declaration source text and Javadoc URLs.  
Adopting Java's static checking rules for the moment, if implementation Foo 
is accepted by the Java static checker when declared:

    class Foo implements Stack { ... }

then it would also be accepted by the static checker when declared

    class Foo implements Queue { ... }

Therefore Foo's programmer is getting the static checker to do the same 
work for him in either case.  Let's call this "enforced correctness".  So if 
the enforced correctness checks are the same, why would Foo's programmer 
elect to declare Foo one way versus the other?  In order to communicate to 
the clients of Foo which of these contracts Foo allegedly does satisfy, 
where the difference lies in the unchecked and not necessarily formalized 
parts of these contracts.  Of course, if Foo's programmer is fallible or 
malicious, he may say "Foo implements Stack" when Foo does not.

Because Java uses (essentially) name-based type equality, Bar's programmer 
may declare a parameter to be a Stack.  This ensures that any argument bound 
to that parameter will 1) meet the enforced correctness criteria of Stack 
(which in this case is the same as Queue), and 2) was alleged by its 
programmer to actually be a Stack.

Both rely(Stack) and suspect(Stack) also fit the above description.  The 
difference is in the significance attached to #2.  rely(Stack) says that Bar 
may depend on this alleging by Foo's programmer.  suspect(Stack) says that 
Bar may not -- it may only depend on the enforced correctness provided by 
the "Stack" declaration.


>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. 

Yes, thank you!  This is indeed what I'm trying to say, and this is a great 
example for explaining it.  However, this isn't quite E for two reasons.  

1) Syntax.  Here it is with syntax corrected:

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

2) Hashing and hash tables are hidden inside the E implementation / UTCB.  
Hash values are not exposed, and hash tables are therefore a primitive type 
in E -- the various kinds of Maps.  This hides the non-determinism that 
EQ-based-hash-values would expose, and it allows E's Maps to avoid relying on 
their clients -- the correctness of an E Map is not vulnerable to the 
objects stored in the map.

However, this example still clearly gets the point across.  I hope to post 
richer examples soon -- perhaps by annotating the examples in the Ode.


> 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. 

Actually, the /*null OK*/ style started in the Xanadu days, probably from 
Dean, Ravi Pandya, Eric Hill, or myself.  It was translated from Smalltalk and 
C++ into Java and Original-E at Agorics and Electric Communities.

> MarkM is suggesting some automatic checking on the part of the
>compiler to warn about certain assignments.

Besides assignments, also variable initialization, including especially the 
binding of an argument to a parameter.  Perhaps some other cases as well, 
I'll know better when I work up a real example.  In any case, this is about 
right for the level of ambition I have in mind.


        Cheers,
        --MarkM