State of the art is translating subsets of Haskell to Isabelle, and verifying them. Using model checkers to verify subsets, or extracting Haskell from Agda or Coq.
Don, can you give some pointers to literature on this, if any? That is, any documentation of a verification effort of Haskell code with Isabelle, model checkers, or Coq?
Graham Hutton's _Programming in Haskell_ has a chapter on reasoning about Haskell code: http://www.cs.nott.ac.uk/~gmh/book.html I put together some exercises of some short proofs for small Haskell functions: http://www.thenewsh.com/~newsham/formal/problems/ I have a short article that covers proofs in Haskell and Isabelle: http://users.lava.net/~newsham/formal/reverse/ The seL4 project is specifying an OS in Haskell, proving it in Isabelle and translating it to C with proofs that connect the translations: http://ertos.nicta.com.au/research/sel4/ I have an article on the curry-howard correspondence http://www.thenewsh.com/~newsham/formal/curryhoward/ In systems like Coq you can write code and proofs of the code in the same language and even at the same time. The Coq'Art book is a good reference, as are Adam Chlipala's draft book and Harvard class materials and the _Type Theory & Functional Programming_ book. Full text for all but Coq'Art are online: http://www.labri.fr/perso/casteran/CoqArt/index.html http://www.cs.harvard.edu/~adamc/cpdt/ http://www.cs.harvard.edu/~adamc/cpdt/book/ http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/
Denis
Tim Newsham http://www.thenewsh.com/~newsham/