[jules]

Incorrect. Haskell's type system cannot ensure arbitrary correctness guarantees. Hence the research into dependently typed languages, like Agda and Coq.