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
(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
Some comments as I'm reading, mostly small nitpicks:
"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?