Lambda the Ultimate

... the non-googlized version of that introductory material url is this.

Conor McBride is known for his terrible puns, but the introductory section of this article is the most spectacular work of his I've seen to date. I hope that he has not given us too much of a good thing...

Of course there are similarities between Wouter's work and mine, in that both connect Hoare-style reasoning and monads. There are also significant differences in approach, as I hope might become evident after more than a skim.

In his paper, Wouter works in the fine old verificationist tradition, attaching logical superstructure to the state monad as we know it, using Coq's Program tactic, one of Matthieu Sozeau's excellent contributions, as a verification condition generator. Your regular

State a = s -> a * s

Pre : s -> Prop
Post : s -> a -> s -> Prop

I work in Haskell, with no logical superstructure. Rather, I use dependent datatypes to create logical infrastructure for the program operations themselves. In particular, I index sets by the 'state of the world': the kind {s} -> * contains type-formers which express properties of a state in type s, but at the same time carry significant dynamic data. This 'state' is not a piece of dynamic store, mutated only by the monadic computation itself; rather it's a static model of possible knowledge about the world, potentially prone to external interference. I use these state-indexed types as data-bearing pre- and post-conditions. Your monadic functions have types like

forall s. p {s} -> m q {s}

where m is a monad on the category of s-indexed types with index-respecting functions, representing some notion of reachability. The type says 'from any state where p holds, you can reach a state where q holds'. In effect, the very definition of a monad for an indexed type gives you a kind of Hoare logic. This property is not specific to monads for mutable store: it's an observation about monads for 'predicates', period.

Meanwhile, I chose an example based on IO exactly because IO does not really behave as predictably as state transforming functions for RealWorld. Indeed, the point is to express the static unpredictability of operations like 'open file': we cannot guarantee statically that they succeed, but we can guarantee statically that we will find out dynamically whether they succeed, and that there will be one bit of data which is known to bear that meaning.

Of course, in a proof assistant like Coq, one could take a 'logical superstructure' view of the same phenomena. My point is that one can achieve at least some improvements of basic hygiene without recourse to a proof assistant, just by baking a little more structure into the program types themselves. Moreover, the 'logical infrastructure' approach is accessible, even with the limited dependent types of Haskell.

Taking a broader view, there is no conflict between logical infrastructure and superstructure. A good programming and proof environment will need to give effective support to both, and the flexibility to move the slider between them to the sweet spot.