Lightweight Static Capabilitites
We describe a modular programming style that harnesses modern type systems to verify safety conditions in practical systems. This style has three ingredients:
- A compact kernel of trust that is specific to the problem domain.
- Unique names (capabilities) that confer rights and certify properties, so as to extend the trust from the kernel to the rest of the application.
- Static (type) proxies for dynamic values.
We illustrate our approach using examples from the dependent-type literature, but our programs are written in Haskell and OCaml today, so our techniques are compatible with imperative code, native mutable arrays, and general recursion. The three ingredients of this programming style call for (1) an expressive core language, (2) higher-rank polymorphism, and (3) phantom types.
Pursuant to this thread about the membrane pattern in static languages from Mark Miller's excellent Ph.D. thesis. I don't yet know whether a solution is derivable from this work, but Mark was kind enough to point me to it, and Oleg seems to want to see it distributed, so here it is—Mark and/or Oleg, please let me know if this is premature.