[e-lang] Joe-E 2.0 Release

[Tyler Close]

On Sat, Mar 8, 2008 at 6:17 PM, David Wagner <daw at cs.berkeley.edu> wrote:
> Tyler Close writes:
>  >Also, rather than have separate safej files, I recommend there just be
>  >a Policy.java file in the Joe-E distribution that contains all the
>  >Java taming decisions. If people want to add more taming decisions,
>  >they edit the Policy.java file.
>
>  Interesting.  Can you say more about why?
>
>  I had thought that safej files were a better way of manually
>  specifying taming decisions, for several reasons: (a) They provide
>  a facility for recording comments about the reasons behind taming
>  decisions; (b) They can be consistency-checked (e.g., if you suppress
>  a method in class C it must be suppressed in all superclasses of C;
>  we can build tools to check this); (c) They are human-readable.

And none of the above can be true of Java code?

>  In contrast, the idea was that Policy.java would be a compiled
>  version of the safej files, for faster enforcement of the taming
>  policy specified in safej files.
>
>  What do you think?  What makes you suggest that the way to extend
>  the taming policy is by editing the Policy.java file?  Does it have
>  some advantages that I've overlooked?  (Simplicity?)

Generating Java code based on safej files creates a requirement for
the developer to be using the Joe-E verifier. I must be able to ship
code that developers can use even if they don't run the Joe-E
verifier. In designing Joe-E, a major requirement was that it was just
a subset of Java, and did not require code transformation. The current
taming design defeats that work by requiring code generation. I want
something that runs out-of-the-box. The current Joe-E distribution
does not.

--Tyler