Re: Capabilities interact nicely with Substructural Types and Reactivity

On Thu, Sep 12, 2013, at 04:13 PM, David Barbour wrote:
> If you know an object isn't stateful - i.e. that it cannot remember its
> past inputs - then whole classes of security, consistency, and
> correctness
> issues can be eliminated. One can prevent time-bomb behaviors that might
> be
> resistant to basic testing and analysis.

I'm on board with this goal.  Joe-E's mechanisms allow you
achieve this goal -- indeed, that was one of the major goals
when we designed the language, and we wrote an entire paper
on the subject.  You should read it. :-)

May I encourage you to take a look at how Joe-E achieves this
and see if it changes your views at all about the adequacy
of DeepFrozen/Immutable for this purpose?

The very short version is that if an object is Immutable, then
you know it cannot remember state; and if you know that all of
a method's parameters are Immutable, then (in Joe-E) you are
entitled to deduce that the method is pure and cannot remember
its past inputs.  This provides a simple, local check to verify that
a method is pure (isn't stateful).  Joe-E was designed to ensure
that this inference would be sound.  (The implicit "this" parameter
must be treated as one of the method's parameters, for purposes
of this condition.)  But read the papers for a detailed explanation.

-- David