I've shared Yegge's disdain for static typing for quite some time. One of the best examples of how awful it can be is type hinting (optional type constraints on parameters) in PHP. Many times I've explained to people why type hints are awful thing deserving banishment to hell — along with Facebook suggestions and Microsoft product recommendations — but so many PHP programmers seem to love them! Now that I read this I…
Also, Haskell is more strongly (and richly) typed than Java\C++\C# so having strongly-typed code works really well.
About proving correctness, I guess you may have seen this amusing piece: http://perl.plover.com/yak/typing/samples/slide030.html
The type system found an infinite-loop bug in the code at compile-time.