Re: [Caja] Important new paper: The Need for Capability Policiies

[Resending at Mark's request: since I wasn't subscribed to e-lang, the
message bounced.]

On Mon, Jul 8, 2013 at 5:58 AM, Meredith Gregory
<[email protected]> wrote:
> P.S. i think what Mike might have been saying about objects is something
> like this.
>
> Which formal model of objects are you choosing in which to prove things
> about the relationship of computations over objects to the particular policy
> language?
> What's the relationship of that formal model to Javascript? As i understand
> it, Javascript is one of the go-to languages for a big portion of ocap
> practice.
> How familiar is the community of ocap practice with the formal model and
> it's relationship to their practice?
>
> There are a few formal models of objects. Which one has wide enough
> acceptance in the theoretical community that there might be enough momentum
> to get it used in the community of practice for use in proving things about
> policy-governed computation?

Yes, that's the gist of it.  Everyone agrees on the rough idea of an
object, namely state + code, but the definition has to be expansive
enough to cover cases where the language doesn't even support
closures; I don't know of a formal definition of "object" that
everyone agrees on, whereas the formal semantics of a pi calculus term
are very clear.

> A similar critique could certainly be levied against a mobile process
> calculus based approach. Mike, are you suggesting that the ocap community of
> practice also look at mobile process calculi for expression of practice
> (writing executable code) as well as proving things about policy-governed
> computation? That's a radical, but interesting idea!

I'm not saying that everyone should switch to programming in Pict, but
rather suggesting that there's a lot of interesting type theory around
pi calculus and that pi calculus satisfies the criteria for being an
ocap language.  It would be really interesting to see, for instance, a
compiler from some subset of JavaScript into some variant of pi
calculus; I think that with some care, the compiler could be light
enough that types could be pulled back from pi to js.  The end result,
I hope, would be insight into how to design a behavioral type system
for general ocap languages.

> For example,
> object-based code is going to suffer the principle port issue, not so for
> process calculi!

I don't think that's really an issue; standard ocap practice is to
factor authority into facets, each of which is a different reference.

> On the other hand, there are not a very many practical
> implementations of process calculi based languages. JoCaml comes to mind.
> Are you thinking of something like that or maybe embedding an implementation
> in a more modern language, maybe like Molecule?

I'm asserting that by understanding process calculi better and their
behavioral types, the ocap community will be in a better position to
accomplish the goal laid out in this paper.

-- 
Mike Stay - [email protected]
http://www.cs.auckland.ac.nz/~mike
http://reperiendi.wordpress.com