The hidden thing about Haskell that makes it super-powerful for expressing safe programs (in my experience) is not only that you can express tight propositions

The hidden thing about Haskell that makes it super-powerful for expressing safe programs (in my experience) is not only that you can express tight propositions in the types. It's that Haskell makes it very easy to write total functions over wider types. When writing OOP code you often start with a number of base assumptions about the input and build the code around them. With Haskell, you make no such assumptions initially and either encode total functions (most of them!) or tighten the types until they match the true system requirements. There are some Prelude functions which violate this understanding (`head` being a classic example). Writing code without these as much as possible makes your code almost guaranteed robust right out of the gate.