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

Nice paper! It's great to have something written down that better
motivates use of the Joe-E verifier.

I had a couple of thoughts while reading the paper than seem worth
incorporating.

+Caller beware+

Section 2.3 on "Untrusted code execution" might seem to be making
slightly stronger claims than can be supported. The section might
leave a reader with the impression that untrusted pure code can be
executed without further worry. For example, the section closes with:

"Once verified as pure, any such plug-in could be downloaded and
executed safely; it cannot gain any information about other private
information stored on the system, nor can it corrupt the state of any
other part of the program."

But a security review would be concerned not only with the direct
invocations made by the plug-in, but also with the invocations the
plug-in can induce its caller to make. For example, a PostScript
renderer plug-in may have an intermediate output that specifies the
names of needed fonts, which the caller should load from the local
filesystem. Though the PostScript renderer doesn't have direct access
to the filesystem, which would break purity, perhaps it can induce its
non-pure caller to access the information and provide it to the next
stage of the plug-in's pure computation. Similarly, a non-pure caller
may have access to a source of non-determinism and inadvertently
communicate this non-determinism to the pure plug-in by the sequence
of calls made, or arguments provided.

+Any Joe-E code can be made pure+

Section 8 on "Discussion" almost says it, but not quite. Any code that
passes the Joe-E verifier can be wrapped in a pure method. So if
you've got some Joe-E code that isn't pure, you can make a pure
interface to it that requires more specific, Immutable arguments and
then calls the non-pure Joe-E code, or constructs new instances of
non-Immutable classes. The moral being that if you've got an algorithm
that you think would benefit from being pure, you can always succeed
in making it pure.

--Tyler

"Verifiable functional purity in Java"
<http://www.cs.berkeley.edu/~amettler/purecomp.pdf>