Haskell and I have a lot in common: we are both advanced, purely-functional, and open-sourced; we both have twenty years of cutting-edge research experience, can develop robust, concise, correct software rapidly; we both have strong support for integration with others; we both have built-in concurrency and parallelism; we are both great debuggers and profilers; we both love our rich libraries and our active community; we both produce flexible, maintainable, high-quality software.
Haskell is a valuable language for a lot of different reasons, but the most important one is that it changes the way that you think about programming. Haskell does things in a very different way from the imperative languages that most of us are familiar with. And it's an extremely well-designed language, so there isn't a ton of crap standing between you and the concepts that you can learn from it.
The number one thing that you'll often hear from functional programming afficionados is that Haskell is referentially transparent, which makes it easy to do things like reason about programs, and write correctness proofs of programs. Writing a correctness proof of a C program (or even an Objective CaML program) ranges from difficult to effectively impossible - the presence of side effects in the code is very hard to cope with in formal reasoning, and when programs get beyond trivial simplicity, they rapidly become intractable for proofs.
Referential transparency is a good thing. But the reason why it's good has very little to do with correctness proofs. The whole "correctness proof" line is silly because no one writes correctness proofs. Real programs - programs that solve real problems - are generally large and complex enough that even if you're using a language like Haskell, writing a correctness proof still isn't practical. Sure, you can easily write a correctness proof for an implementation of a binary search tree in Haskell. You can write a correctness proof for that in, say, Java. But the Haskell proof will be easier and cleaner, and you'll be able to trust the connection between the code and the proof much more than you could in Java. But really, a good set of tests - which you should be writing, whether you're programming in Java, C, or Haskell - does as good a job of verifying the correctness of something simple like that. And for anything significantly more complicated than that, people just don't write proofs. I've certainly never seen a correctness proof for a Haskell program, except in papers arguing about how provable correctness is in Haskell. (Does GHC have correctness proofs? I doubt it. It's certainly had quite its share of bugs, which means that either it's correctness isn't proven, or the proof is wrong!)
So what makes Haskell so wonderful? Or, to ask the question in a slightly better way: what is so great about the pure functional programming model as exemplified by Haskell? The answer is simple: glue.
Languages like Haskell have absolutely amazing support for modular development. You build the basic semantics of your system in terms of primitive functions, and then the language provides tons of very elegant glue for putting the pieces together. In an imperative language, the fact that the order of execution is highly constrained by side effects means that the ways of connecting components are limited by the fact that you could break things if the glue doesn't work quite right.
But the basic properties of Haskell make it much easier to build generic glue. Lazy evaluation combined with no side effects means that many of the problems that make generic glue difficult in imperative languages just simple don't exist in Haskell. You don't need to worry about whether the iteration glue will correctly ensure that array element n is updated before array element n+1; lazy evaluation will take care of making sure that the data dependency order is respected. And the fact that building new functions, and currying existing ones is a lightweight, syntactically trivial operation means that the glue can be written clearly and concisely.
The Monad concept, which I'll get to in a later post, is an amazing example of this. Monads are a basic tool for sequencing: when things need to be done in sequence, the Monad constructs allow you to make that happen. But there's not just one monad that does sequencing. There's a basic concept of what a monad is, and anything you implement that fits that concept can use all of the monad tools provided by a language. So I can use the same constructs for writing sequencing code for list processing, for performing IO, for writing numeric code that does updates to mutable arrays, for combining non-deterministic computations, and more.