[Haskell-cafe] Re: Verifying Haskell Programs

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.

Another state of the art is to use type classes, GADTs, and/or type functions, to specify and prove the properties you want about your program. Basically using similar techniques as used in dependently typed languages. Stefan