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

[+sophia, +james]


On Tue, Jul 7, 2015 at 4:47 AM, Mark Miller <[email protected]> wrote:

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


-- 
    Cheers,
    --MarkM

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