[E-Lang] Other E News: E & EROS

[Mark S. Miller]

As I'm about to be gone for a week, now's a good time to update y'all on 
some other E relevant developments.  In this message, news regarding E and 
EROS.



                        E to be EROS's Shell Language

At the EROS workshop, Jonathan wrote on the whiteboard a very good list of 
the tasks that need to be done to turn EROS is a practical and useful 
system.  When we discussed what their relative order should be, I was 
pleasantly surprised to see consensus that "shell / command line 
interpreter" was one of the first things to do.  Everyone was very happy 
with the idea of an ENative-like implementation of E being used as EROS's 
shell language, and for E's notions of capability & capability invocation to 
be mapped naturally to EROS's.

                           http://www.CapIDL.org

However, in order to do this, another piece of infrastructure must first be 
built: an interface definition language (IDL) must first be defined which 
can describe (at least) EROS capability invocations in terms of the data 
types that programming languages traffic in, all the existing capability 
protocols must be described in terms of this IDL, and a query must be added 
by which one can ask a key for the IDL (or a predigested equivalent) that 
describes its protocol.  Finally, for each supported language, an IDL 
compiler is needed to generate the marshalling and unmarshalling code that 
interfaces EROS to the concepts of that language.

Towards this end, I've proposed CapIDL, and IDL designed initially to 
support EROS specifically, but intended to be able to grow into something 
that can serve more generally as a basis for interoperability between 
capability systems.  Just as E was designed to look familiar to C and Java 
programmers, CapIDL is designed to look familiar to Corba programmers.  Not 
to enable the porting of Corba *.idl files, but to port Corba programmers.  
The eros-arch list has been intensely discussing CapIDL for a while, and the 
current draft proposal owes much to these discussions.

The current draft proposal is posted at the above URL


                      Jonathan & I fix each other's formalisms


I'd been developing a growing discomfort with the tradition among OS folks, 
starting with Butler Lampson, at formalizing capabilities.  While I think 
Jonathan's formalism may be better in many regards, at its heart it still 
held that nugget I found disturbing.

In a conversation following the workshop in with Jonathan, Scott, Ben, and 
myself, I showed how Jonathan's formalism of capabilities -- a pair 
designating state & a *set* of operations (equivalently, state & interface 
type) -- could not even describe EROS itself.  In EROS, as in most other 
capability systems (including KeyKOS, E, Joule, and W7), two different 
capabilities designating the same state could respond to the same message 
(order code) with two different behaviors.  To describe this requires that 
we replace the "set of operations" with a "mapping from order codes (ie, 
message names) to operations", ie, a vtable.

Of course, objects don't have to dispatch on the order code, so we ended up 
with a two level description.  The fundamental level of description has a 
capability be a pair of a state designator and a behavior designator.  The 
behavior is a procedure of two arguments -- the state and the incoming 
message.  All the information that determines the object's behavior on 
invocation must be reachable from the behavior, state, and message.  At a 
non-fundamental level, if the behavior starts by switching on part of the 
message (the message name / order code), then we have a vtable-like mapping.

This formulation makes clear the unity of EROS's (and KeyKOS's) capabilities 
with lambda calculus based programming languages, especially those in the 
Actors tradition.  Including especially E, as the multi-facet nature of E 
maps very well to the multi-facet nature of EROS.  The fact that OS 
formalists have been getting this wrong till now may also help explain why 
they've been underestimating capabilities.  Specifically, if you don't see 
the mapping, you don't see the polymorphism.  More on this later.
If Jonathan & I can find the time, we've agreed to coauthor a paper on this.

There has also been much discussion on the EROS list of this shift in 
perspective, and how it should or should not effect the way we speak 
informally.  No clear results so far.


But my capabilities formalism was totally broken.  It couldn't work at all.


I gave two talks, on E and on Smart Contracts, both of which were well 
received.  During my E talk, I put up my "one slide definition of capability 
security", which is essentially identical to 
http://www.erights.org/elib/capability/ode/ode-capabilities.html#patt-coop . 
Jonathan pointed out that there's a 4th way in which Bob can come to have a 
capability to Carol: "Connectivity by Initial Conditions".  Indeed, without 
this, none of the rest ever apply.  If "Only Connectivity Begets 
Connectivity", we're in trouble unless we posit a world with some initial 
connectivity.


These are good cautionary tales for why proofs of correctness are hard.  If 
we call our formalisms "specifications", then both of us built systems that 
did not meet our specifications.  In both cases, the systems were right and 
the specifications wrong.  

        Cheers,
        --MarkM