On Sun, Feb 1, 2009 at 12:54 PM, Paulo J. Matos
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/