[cap-talk] Abstractions that subsume capabilities

[Sandro Magi]

Sandro Magi wrote:
> 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.

Upon further thought, this requires further elaboration. Progress is 
made when building on existing knowledge, and this process presumably 
results in fine-grained distinctions which are important to deep 
understanding of a subject.

When considering capabilities from a language perspective, there are not 
as many novel properties as there are from the OS perspective. As I 
quoted above [1], the object-capability model is effectively the 
lambda-calculus. The novelties of object-capabilities in this setting 
aren't protected, unforgeable descriptors, since the lambda calculus 
already has lambda names. The "reference graph = access graph" 
equivalency is already present.

The novelty of capabilities for programming languages is thus in 
*controlling access to effects* via the reference graph. From this 
perspective, techniques to preserve referential transparency in the 
lambda calculus and capability security restrictions to languages built 
on the lambda calculus to control "world" effects are directly comparable.

MarkM's thesis [1] distinguishes "primitives", which are internal to the 
language, and "devices", which are external. Most languages provide 
ambient access to devices resulting in all the current problems in 
isolating subsystems.

Both capabilities and RT techniques impose restrictions on the use of 
effects which affect the "world", ie. via devices. In Haskell, this 
distinction is not very fine-grained at the moment, as most effects 
simply live in the "IO" monad, but there is no reason why these effects 
couldn't be made more fine-grained, ie. IO => DelDir, SendPacket, etc.

When combined with types, RT is a powerful reasoning tool. RT further 
tends to increase modularity and reuse, which helps with code 
correctness, so there are compelling software engineering benefits as well.

I hope that clarifies the distinction I was trying to make.

Sandro

[1] I can't seem to access the thesis at the moment