That's where formal proofs come into play, because you need to somehow show that the implementation actually does what the definition states. Since Haskell isn'

That's where formal proofs come into play, because you need to somehow show that the implementation actually does what the definition states. Since Haskell isn't a proof checker you can't use it for this. The newish and very promising looking language Idris [1], which is very similar to Haskell, can actually do this because of having dependent types. Upon a quick search I found this great example [2] of a proof that insertion sort does indeed return the list sorted, all in the type system. I can really recommend Type Driven Development [3], a recently released book on development in Idris. [1]: https://www.idris-lang.org/ https://www.idris-lang.org/ [2]: https://github.com/davidfstr/idris-insertion-sort https://github.com/davidfstr/idris-insertion-sort [3]: https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...