Monadic Library for Eio Capabilities?

Learning
38

When I read all this, two questions come to my mind:

  1. why do we try to impose capabilities on the entire community by encoding them into Eio?
  2. why can’t we deal with capabilities by integrating formal verification with OCaml and expressing capabilities at the formal specification level?

To elaborate on 1:

  • Having to deal with capabilities comes as a surprise when you’re coming to OCaml from other ecosystems. This has nothing to do with the length of the code, or having to touch many places when the need for capabilities changes as the application evolves.
  • In a business context, you are looking at tradeoffs such as development speed versus reliability. Many times, over the trajectory of a project, these needs change. With its unobtrusive and convenient type inference, OCaml is very well positioned as a language that allows you to rapidly prototype (and later achieve increased reliability by adding .mli files to solidify the interfaces). IMO, capabilities are exactly one such means to achieve increased reliability. Making this choice of trading development speed (developers needing to understand what capabilities are and why you should care) for increased reliability at the ecosystem level is IMO a mistake. It positions OCaml towards a niche audience that values reliability over development velocity. In particular, it would make the OCaml ecosystem less attractive to startups who need to optimize for quick development. That is, assuming, that the broader community maintaining the OCaml ecosystem will even adopt Eio.

To elaborate on 2:

  • What if we address the needs of different parts of the OCaml community, and different project stages by creating a good developer experience for using formal verification in OCaml?
  • With the development speed vs reliability tradeoff and how that impacts OCaml’s viability as a language for various projects and businesses, it seems only natural to me that there’s a progression along these lines: writing .ml files only for prototyping > adding .mli files > adding Gospel formal specification. So with every “layer” here, we add more reliability, but we incur a cost (which is often worth to pay in the long run, but usually not worth to pay in the short term before a project is fully validated).
  • IMO, something like capabilities belongs into the formal verification layer as it introduces complexity that small projects should not need to incur.
5 Likes