Re: Comments requested on paper: functional purity in Joe-E

That's a seriously interesting paper. It never occurred to me how useful
the Joe-E overlay type system could be for program verification until
now. 

(It looks like this work leverages some of the "best of both worlds"
between work on languages and process calculi. Lots of work on process
calculi, such as those derived from the pi-calculus, has focused on
developing type systems for verifying similar properties. This work
appears to "lift" that to a real-world language, leveraging properties
of the object-capability model (e.g. references can only be passed on
other references) to ensure the type system is sound. This is comparable
with the process calculi work which often leverages properties of the
underlying calculus (e.g. names can only be communicated via other names
in pi-calculus) to ensure their type systems are sound. However, your is
inherently more useful since people actually happen to write real code
in Java.)

Some comments as I'm reading, mostly small nitpicks:

Sect 3:

"In particular, references serve as capabilities, and capabilities can
be granted only be explicitly passing references. For instance, the
global scope must not cantain any capabilities."

That second sentence sounds problematic. Surely the global scope does
contain capabilities, e.g. capabilities to constructors to safe classes
and those to immutable objects, right?


Sect 4.3:

Consider changing "Similarly, we treat null pointers as references to a
canonical null object belonging to every type." to
"Similarly, we treat null pointers as references to a single coninical
null object that belongs to every type.". When I read the original
sentence, I misinterpreted it to mean that there was a different
canonical null object for every type -- not that there was a single
canonical null object that could be considered to be of every type.
Perhaps this was just me not paying close attention...


Sections 3 to 5:

The paper states, informally, what immutability is. It also informally
defines side-effect freeness. It formally defines determinism in terms
of equivalence of reference lists, which is itself fairly formally
defined. It then says that functional purity (which requires both
determinism and side-effect freeness) can be enforced by ensuring access
to only immutable objects.

I don't see why the formal definition of determinism is given at all,
since it is never connected with the idea of immutability via
equivalence. Instead, only informal arguments are given in Section 5
that having access only to immutable objects (and the rules of the
object-capability language) gives rise to determinism. Unless
immutability is defined in terms of equivalence, one cannot use access
only to immutable arguments to imply determinism -- at least not
formally. This problem doesn't exist with side-effect freeness since it
is only defined informally. However, it makes the argument that
side-effect freeness is enforced only an informal one. 

Instead you could

 -- define immutability in terms of equivalence
 -- use this and the properties of the object-capability model to prove
that a method with access to only immutable arguments is in fact
deterministic, or at least sketch out this argument
 -- define side-effect freeness in terms of immutability
 -- use this and the properties of the object-capability model to prove
that a method with access to only immutable arguments is in fact
side-effect free, or at least sketch out this argument

As the paper is, the reader must make this connection themselves. It
also makes (to me) the trouble of defining determinism formally a bit of
a distraction, since this formal definition is not used in the arguments
that immutability implies functional purity. It is a logical and natural
one to make, but I would argue that it should be being made explicitly
and formally by the paper and not implicitly by the reader.

That said, I'm probably being far too picky here. I expect you've
included as much of the details as you can without going over budget on
length and understand that these sorts of tricky trade-offs always need
to be made.
 

(Am yet to read past Section 6 but might pester with more comments about
later sections as I read them.)

Cheers again for such a cool paper. I'm really enjoying reading it and I
think the ideas it embodies are really powerful -- mostly because of
their inherent usefulness to verifying real properties on real code.
It's a very refreshing alternative to my own work.

Cheers

Toby

On Tue, 2008-06-03 at 23:00 -0700, Adrian Mettler wrote:
> Resending with URL instead of attachment, as it appears moderator 
> approval isn't happening:
> http://www.cs.berkeley.edu/~amettler/purecomp.pdf
> 
> -
> 
> David Wagner and I have recently submitted our first paper relating to
> our work on Joe-E, an object-capability subset of Java.  It focuses on a
> simple pattern that ensures that a method is side-effect free and
> behaves as a deterministic function of its arguments (i.e. invocations
> with equivalent arguments will yield equivalent return values) and how
> this property can be used to verify security properties.  We would be
> interested in comments from more people in order to improve the paper.
> There's a fair amount of time before any camera ready would be due (it's
> still a while before committee decision comes back).
> 
> Thanks,
> Adrian
> 
> 
> 
> _______________________________________________
> e-lang mailing list
> [email protected]
> http://www.eros-os.org/mailman/listinfo/e-lang