Software with formal properties at a low cost through monads and co-execution

Not so long ago a good friend of mine mentioned his need for 'formal properties' in his code.  

I asked him if he had already made the code purely monadic. He had. "Good", I said, "because the 'cheap route to formal properties' is first to ‘monadize' your code, and then 'reverse it' by bringing in 'co-execution'".  That last part needs some development. 

Formal properties are not only about execution, actually mostly not about execution, but more about formal properties of state. So while you do need to show execution invariants, you often much more need to show that the ‘results’ happen within stateful invariants (e.g. of the ledger). The easiest way to do this is to  deconstruct / co-execute the state model backwards. This 'backwards' logic must 'match-up' with the 'forward execution' (monadic) model. My view has always been comonads are easiest for this, especially if your stateful model (e.g. a blockchain) is already something that is easy to express as a comonad. 

You might note that my last post is all about combining 'forward' and 'backwards' arrows. One way to interpret these arrows is 'right arrow' for monads, and 'left arrows' for comonads. And sure enough, that is an easy way to sketch out higher order systems where adjoint invariant properties (e.g. rights, expectations, authorizations, ...) are assembled 'with good properties' by design. As mentioned in previous slide, monads are easy to express as CPS, and as are comonads with a bit more 'gymnatics' (see previous post).

All original content copyright James Litsios, 2022.