Re: Capabilities interact nicely with Substructural Types and Reactivity

DavidB, I think the discussion is getting side tracked by a minor point. I
tried reading your first message on this thread. It sounds cool but I don't
actually understand it either. If it could be restated in terms more of us
could understand -- especially non-type-theorists -- I suspect we'd all be
quite interested.

Concrete example would help tremendously!



On Thu, Sep 12, 2013 at 5:38 PM, Mark Miller <[email protected]> wrote:

> This is a difference from E. This paper shows how to leverage Joe-E's
> Immutable to determine purity. This is cool and there isn't anything like
> it in E.
>
>
> On Thu, Sep 12, 2013 at 5:29 PM, David Wagner <[email protected]> wrote:
>
>> 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
>> _______________________________________________
>> cap-talk mailing list
>> [email protected]
>> http://www.eros-os.org/mailman/listinfo/cap-talk
>>
>
>
>
> --
> Text by me above is hereby placed in the public domain
>
>   Cheers,
>   --MarkM
>



-- 
Text by me above is hereby placed in the public domain

  Cheers,
  --MarkM

_______________________________________________
cap-talk mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/cap-talk