[cap-talk] Abstractions that subsume capabilities

[Sandro Magi]

David-Sarah Hopwood wrote:
> Sandro Magi wrote:
>> Interesting coincidence: I had just kicked off a debate on LTU that 
>> referential transparency subsumes capability security [1]. I'm curious 
>> what people here think as well.
>>
>> Sandro
>>
>> [1] http://lambda-the-ultimate.org/node/2706#comment-40510
>>     
>
> I agree with almost all of Peter van Roy's comments [*]. In particular,
> referential transparency does not imply capability security, because it
> does not imply encapsulation.
>
> Encapsulation is independent of state -- immutable data can be kept
> private by encapsulation. Consider, for example, a 'signer' object that
> holds a private key, and will cryptographically sign given data using
> that key (using a secure algorithm that is assumed not to leak key
> information). This object is referentially transparent, but whether it
> can keep the key secret depends on other attributes of the language;
> it isn't automatic that the key is kept secret because the object (or
> any term in the language) is referentially transparent.
>   

Ah, the perils of imprecision and unstated assumptions. :-)

When speaking of referential transparency, I am of course speaking of it 
in terms of programming languages, and the lambda calculus at a minimum. 
A lambda is encapsulated.

In Section 9.1, footnote 1 of MarkM's thesis, he defines the 
"object-capability security model" as:

  Our object-capability model is essentially the untyped call-by-value 
lambda calculus with
  applicative-order local side effects [...]

Preserving referential transparency eliminates the dependency on 
evaluation order, while preserving all of the language's other 
properties that I can see. There might be a small hit to expressiveness 
due to more tightly controlled side-effects, but I think this is largely 
compensated for by the increased reasoning power over effects.

This exchange and the debate has been very illuminating!

Sandro