>>Except that there is a real advantage to using pure functional programming; being able to easily prove theorems about your code and understand different components in isolation.

How much of the Haskell (a pure FP language) library code is formally proved? Just curious.

Also I wonder, if code like xmonad can be proved at all.