[E-Lang] Reliance & Static Security Checking

Mark S. Miller markm@caplet.com
Thu, 04 Jan 2001 15:02:23 -0800

At 08:04 AM Tuesday 1/2/01, Karp, Alan wrote:
>There is one aspect that I think is immediately implementable, and he has
>given an example of it.
>>     def a : rely(Foo)
>>     def b : suspect(Foo)
>> then
>>     b := a
>> looks ok, but
>>     a := b
>> is cause for alarm.
>Just this amount of static checking would prevent errors involving reliance
>on data declared unreliable; things can only get less reliable, not more so,
>sort of like entropy.
>What, then, could "rely" mean?  

The correctness of the objects containing this variable "a" depends on "a" 
only holding values that correctly obey the "Foo" contract.

>Well, where can I put my checks?  I see only
>two places, inside the object or where its result is used.  

The two places I'd proposed are 1) On a variable definition, which, in E, is 
a pattern that serves as a defining occurrence of a variable.  The variable 
so defined may, in conventional terms, be a parameter variable, local 
variable, or instance variable, or it may serve several of these roles.  2) 
On a method result declaration.  To reiterate, "rely(Foo)" on a method 
result says that those who rely on the object containing this method may 
also rely on the result of the method to be a correct Foo.  Put another way, 
if the containing object returns an incorrect Foo, then it is also not correct.

Other choices are possible, and may even be crucial for this proposal to be 
useful.  The above two are simply the first things I thought of, since 
that's where E's guard expressions (soft types) currently appear.  If by 
"where its result is used" you mean an invocation expression, this is not an 
option I'd considered.  It may well be a good one.

>Let's say that
>"rely" means that I'm depending on the object to do all checking (type,
>error, security, whatever); 

Not my intention at all.

>"suspect" means that I'll take care of verifying
>the part of the result that I need for this use of the function.

This may be what I meant, depending on which party you mean by "I".

>"rely" means that the object has been debugged, or maybe even proven
>correct; suspect means I'll check myself.

I think it's fair to say that your "rely" has nothing to do with mine.

>Here's an example from an early e-speak implementation in Java.  I wanted to
>have a homogeneous collection, but Java 1.1 collections only take Object.
>In my first implementation, I made every effort to put the same kind of
>thing into a particular instance of the collection, but then I had to check
>that I had the right type every time I pulled something.  I'd call this
>collection "suspect" with respect to result type.  I hated that approach and
>eventually found a way to guarantee that the collection could only hold the
>right type of object.  (Override the add() method so the compiler does the
>checking.)  I was able to eliminate all the checking.  I'd call this second
>version "reliable" with respect to return type.

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

For those (like me) that like to anthropomorphize we may say "A believes B 
is correct", but only so long as we don't confuse A with A's programmer, and 
only so long as we don't take it to imply that A has some objective reason 
for believing B is correct.  Rather, "A believes B is correct because A was 
built to believe B is correct."  This is probably also too confusing a way 
to speak.