Typed Functional Programming and Software Correctness

I'm sure you've all heard Haskell programmers say that if their code compiles, you can be sure the program is correct. I'd found that hard to believe until I tried building something in Haskell: the type system lets you describe the properties of your data and behaviour. When you compile, the theorem prover inside GHC verifies that your code obeys the described properties.

This article does a good job of showing some flaws within the development experience of mainstream languages as well as showing how a typed functional languages can address them.

It does make me wonder why FP isn't more popular. Is it because of the high level of abstraction? Sure, you need to learn what a monoid, or an functor is. But once you do that, you can use the interface and behaviours described by these categories to interact with _any_ other monoid / functor, no matter who wrote it or what it achieves.