I think the “Haskell programs just work” thing is overblown. It’s true that once they compile, they are more likely to work than a program compiled in a language with a weaker type system than Haskell’s, but just because you can leverage the Curry-Howard isomorphism to validate some parts of your code, the bulk of that code is still… well, code. Function bodies. And CH will not help you there.