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/

[2]: https://github.com/davidfstr/idris-insertion-sort

[3]: https://www.manning.com/books/type-driven-development-with-i...