Re: Capabilities interact nicely with Substructural Types and Reactivity

On Thu, Sep 12, 2013 at 3:00 PM, David Wagner <[email protected]> wrote:

> I admit I'm puzzled by your email.  Have you looked at
> E's DeepFrozen and Joe-E's Immutable in detail?


Yes. I've even reviewed it again now to double-check my understandings:

  http://www.eros-os.org/pipermail/e-lang/2005-January/010418.html
  http://www.cs.berkeley.edu/~daw/papers/pure-ccs08.pdf



>
> I confess I don't understand how using immutable/DeepFrozen
> objects/types is "selling out", but maybe that just reflects a
> difference in values or philosophy or something.


I would like to clarify:

DeepFrozen and Immutable are practical ways to solve real problems.

But they are achieved by reflection and type systems, outside OOP and
object capabilities.

Therefore, it is unreasonable to point at objects or capabilities as
providing the answer.

Further, DeepFrozen and Immutable do not have the same fine-grained
security-by-composition benefits as object capability model; they do not
enable the deep interleaving of trusted and untrusted code. They are very
blunt force tools.


> Despite what you write, in Joe-E, the Immutable type does
> not forbid code from constructing its own local mutable state.
>

There are two separate issues here:
* to me "state" means the ability to accumulate information over logical
time (e.g. across events)
* when multiple values represented at a single logical time, this is called
'space'

Imperative languages tend to confuse the two, because sequencing over
'time' is so heavily part of their control-flow model. But in a more
precise language, especially in dataflow models, the two roles can often be
formally distinguished.

What Joe-E enables is a representation of a stateful algorithm internally,
but this corresponds to a single logical instant (a single function call)
externally. Therefore, it is really 'space' with regards to the external
world, and one could literally distribute the computation over space by use
of time-indexed variable names. A useful distinction between the use of
space modeled statefully vs. real state is that there are no concurrent
interactions from independent entities.


>
> Contrary to what you write, Joe-E's Immutable type does provide a
> way to ensure determinism.


Indeed. It uses type analysis to complete the job (ensuring the output type
is immutable), which DeepFrozen does not.



Generally speaking, in a capability design, if you want to let untrusted
> code access some capabilities and not others, a typical strategy
> is to pass the untrusted code the capabilities you want it to have
> access to and take care to never pass it the capabilities you don't.
>

Indeed. But this only works for capabilities, not for ambient authorities.
If you wanted to control access to `new`, or restrict code to using a pool
of audited state provided by you, this could not be expressed in most OOP
or object capability languages.

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