JohnDEarle:
You may want to look into Objective CAML http://caml.inria.fr/ which is a French product as you can see from the Internet address. It is likely better suited to the task than Haskell and has a reputation for speed. For those who prefer object oriented programming it has facilities for that which may ease your transition from C++. The Microsoft F# language is based on Objective CAML.
Haskell has a problem with its type system and is not rigorous. Haskell is not a suitable language for proof assistants and so I would advise you to stay clear of Haskell. Standard ML was engineered with the needs of proof assistants in mind and so you may want to look into Standard ML, but you should be very happy with Objective CAML. It has an excellent reputation. The Coq proof assistant which is another French product is based on Objective CAML.
Ok, that is serious trolling. There are several proof assistants written in Haskell: http://hackage.haskell.org/package/Agda http://hackage.haskell.org/package/ivor http://www.e-pig.org/ http://wiki.di.uminho.pt/wiki/bin/view/PURe/Camila http://www.cwi.nl/~jve/demo/ http://www.haskell.org/dumatel/ http://www.cs.chalmers.se/~koen/folkung/ http://taz.cs.wcupa.edu/~dmead/code/prover/ http://www.math.chalmers.se/~koen/paradox/ http://proofgeneral.inf.ed.ac.uk/Kit http://www.haskell.org/yarrow/ and the guarantees of purity the type system provides are extremely useful for verification purposes. Please, before posting like this to the Haskell community, inform yourself more of what the Haskell community has produced. -- Don