Fare's meta-protocol

[Mike Prince]

On Fri, 23 Dec 1994, Francois-Rene Rideau wrote:
> ### The meta-protocol ###
> 
>    The meta-protocol itself is a protocol, and thus is purely conventional
> and may be replaced or upgraded. Of course, as always, we'll provide the
> best one, so nobody will have to get one from third-parties, but they may
> if they like or need.
>    It will typically include some type-checking, differenciating types to
> be at least no weaker than the GC (that has to differentiate data from
> pointers), but that may be stronger. Multiple type systems correspond to
> multiple meta-protocols (or sub-protocols of it). Stronger meta-protocols
> will also require some correctness proof. The proof may include
> arguments like "object X (with argument Y) told it was true" to simplify, so
> that if you don't trust, but trust X and Y, you may ask object X with argument
> Y about what it thinks. Multiple proofs may be provided, so that if the
> loader trusts object X1, but not object X2, you may prove using either X1 or
> X2. The proof itself may require outer modules, that may have to be loaded,
> etc; but the loader will ensure that no more resource will be allocated to
> the object than the object is allowed.
>    As for the standard type system, I'd recommend one much like the Coq
> proof system uses.

What I'm really asking is what's the format?  And all I keep hearing is 
we'll specify it later.  I'd like to see some pseudo-format for how 
exactly you plan to do it.  Everything above is really gray.  It also 
looks like it would balloon the size of objects in transit.  It also 
looks complicated and would require more resources that other 
alternatives.  Please propose a format so we can evaluate it.

Mike