[Haskell-cafe] Verifying Haskell Programs

[Thomas DuBuisson]

On Sun, Feb 1, 2009 at 12:54 PM, Paulo J. Matos <pocmatos at gmail.com> wrote:
> What's the state of the art of automatically
> verifying properties of programs written in Haskell?

This is a large field that isn't as black and white as many people
frame it.  You can write a proof [1] then translate that into Haskell,
you can write Haskell then prove key functions, using a case totality
checker you could prove it doesn't have any partial functions that
will cause an abnormal exit [2], some research has been performed into
information flow at UPenn [3], and SPJ/Zu have been looking at static
contract checking [4] for some time now - which I hope sees the light
of day in GHC 6.12.  While this work has been going on, folks at
Portland State and a few others (such as Andy Gill [8], NICTA [5], and
Peng Li to an extent) have been applying FP to the systems world [6]
[7].

Hope this helps,
Thomas

[1] Perhaps using Isabelle, isabelle.in.tum.de.
[2] Neil built CATCH for just this purpose (though it isn't in GHC
yet), www-users.cs.york.ac.uk/~ndm/catch/
[3] www.cis.upenn.edu/~stevez/
[4] www.cl.cam.ac.uk/~nx200/
[5] http://ertos.nicta.com.au/research/l4/
[6] Strongly typed memory areas, http://web.cecs.pdx.edu/~mpj/pubs/bytedata.html
[7] Some work on non-inference as well as thoughts on building a
hypervisor, http://web.cecs.pdx.edu/~rebekah/
[8] Timber language - no, I haven't looked at it yet myself.
http://timber-lang.org/