Re: [friam] Formal modeling of systems based on E/CapTP/(Water)Ken/Cap'n Proto ideas

On Tue, Jul 7, 2015 at 12:10 AM, Dan Connolly <[email protected]> wrote:

> On Mon, Jul 6, 2015 at 3:59 PM, Mark Miller <[email protected]> wrote:
> > IANAF -- I am not a formalist. But my co-authors (Sophia and James,
> cc'ed) are. Today at PLAS (Programming Languages and Security) Sophia
> presented
> >
> > Swapsies on the Internet: First Steps towards Reasoning about Risk and
> Trust in an Open World
> > <http://research.google.com/pubs/pub43808.html>
>
> Very interesting. I'm just starting to read it; first detail that stands
> out:
>
> "We model private fields as they are simpler than nested lexical scopes"
>
>
Both of my coauthors already know that I strongly disagree with that ;).

That said, here's the way in which I think it is true and relevant. In, for
example, E or W7, the instance variables of an object (i.e., closure) are
simple the lexical variables that it captures. In FOCaL, the classes are
all top level, and the instance variables of its instances are explicitly
enumerated in the class. If you want to reason about connectivity as we do,
this explicit enumeration is helpful. Put another way, simple top level
classes are a lower level representation that a lambda language can compile
to by the following transformation:

     .... (lambda ... x ... y ...) ....

where x and y appear freely within this lambda expression itself, and
therefore are captured from the lexical context. IOW, x and y are instance
variables of the closures this lambda expression evaluates to. Given unique
name f and ignoring side effects, this is equivalent to

     (def (f x y) (lambda ... x ... y ...))
     .... (f x y) ....

By applying this transformation repeatedly, we move all lambda expressions
to be directly under a top-level def in this way. A top level def whose
body is a single lambda is equivalent to a class whose instance variables
are the f's parameters and whose behavior is the behavior of that lambda
expression. The top level scope of such a program consists only of class
names such as f, which are therefore the only variables that these class
definitions can use freely. Other than those, they are closed.

To account for side effects to shared variables, we would need to first do
the usual trick of replacing shared variables that are assigned to with
slot objects (so-called "references" in ML or "boxes" in Sophia's
terminology) where reading and writing the original variable turns into get
and set operations on the slot. The variables serving as class names are
assumed unassignable and so would not be subject to this "boxing".

Coauthors, does this adequately capture the lambda vs class equivalence you
have in mind?




> --
> Dan Connolly
> http://www.madmode.com/
> _______________________________________________
> cap-talk mailing list
> [email protected]
> http://www.eros-os.org/mailman/listinfo/cap-talk
>



-- 
Text by me above is hereby placed in the public domain

  Cheers,
  --MarkM

_______________________________________________
cap-talk mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/cap-talk