(joint with Dana Xu, Cambridge Computer Lab)
Modern type systems (eg in Haskell and ML) exclude many bugs by construction. But not all! We would like to go beyond these type systems, and write down the pre and post-conditions of our functions. More generally, in a higher-order language like Haskell, we extend traditional pre/post conditions to so-called "contracts.
Then we are faced with questions like
In my talk I'll describe work in progress that makes some progress on these questions, in the context of Haskell. Our goal is to extend the "reach" of static verification, beyond traditional type systems, and to do so in a way that ordinary programmers (without PhDs) can make sense of.