"Recovering Purity with Comonads and Capabilities"

16 views

Skip to first unread message

Mark S. Miller

unread,

Aug 28, 2020, 9:45:42 AM8/28/20

to cap-talk, Discussion of E and other capability languages, fr...@googlegroups.com, SES Strategy, Sophia Drossopoulou, James Noble, Toby Murray, Eisenbach, Susan, Darya Melicher, Jonathan Aldrich, Alex Potanin, Gardner, Philippa A, Alan Schmitt, Jonathan Shapiro, Dominique Devriese, Vikraman Choudhury, Neel Krishnaswami, Colin Gordon, David Swasey, David Swasey, Philipp Haller, Sylvan Clebsch, Sylvan Clebsch, Elias Castegren

We need to continue the conversations about formal methods for capabilities, ocap reasoning about effects and authority, specifying security properties of ocap programs, etc. The following paper seems like a good place to start:

https://arxiv.org/abs/1907.07283

I am not a formalist, and so do not follow many of the details in this paper. But what I do follow seems important. It looks like it accomplishes in the type system the same distinction that the E auditors call "DeepFrozen" and the Joe-E auditors call "Immutable". Like Wyvern, they call this distinction "Pure", which is also the way we've been using the term in SES --- without yet a way to check for it. (This is in contrast with an earlier definition of pure in PL which they discuss and which we may now treat as historical.)

Separately, I found intriguing their discussion of the relationship between linear logic, separation logic, and reasoning about the denial of capabilities in section 8.

I suggest that further discussion happen on the cap-talk list. To participate please join at https://groups.google.com/g/cap-talk . The group is otherwise low volume, and would be a natural home for these topics.