Re: Capabilities interact nicely with Substructural Types and Reactivity
David Barbour <[email protected]>
| Newsgroups | gmane.comp.capabilities.general |
|---|---|
| Message-ID | <CAAOQMSsNZASH6cmS3SQr_uk6qKosZFNvV0et1=YgSdCL4Z5sTQ@mail.gmail.com> |
What 'compositional' means to me is that you can built two independent software components, combine them with 'composition operators', and reason about them in terms of high-level mathematically inductive properties, without knowing their implementation details. A KeyKOS factory is compositional in the naive sense that two factories can be combined to create a larger factory. Unfortunately, it is generally not the case that two whitelists can be combined to create a bigger whitelist - i.e. you may want different authorities in different software components. The resulting specialization violates compositional reasoning. Use of a powerbox with a textual representation of code is a much more compositional design. On Thu, Sep 12, 2013 at 3:33 PM, Mark Miller <[email protected]> wrote: > I would be interested in your opinion about whether the KeyKOS Factory > with whitelist is compositional in the way you mean. It is certainly > compositional in many ways, but I don't know precisely what you mean here > by compositional. > > _______________________________________________ cap-talk mailing list [email protected] http://www.eros-os.org/mailman/listinfo/cap-talk