Functional vs Imperitive Programming

I was just comparing the qsort algorithms in Haskell and the ones written in C++. The pseudo-code in CLRS is surprisingly more complex than the one in Haskell, and takes much more time to understand and walk through than the one written in Haskell. I'm guessing that a similar implementation in Scheme or ML would have the same sort of expressiveness. I think the real comparison will be when a programmer or algorithm designer can compare the proofs of correctness of an algorithm. I think that a proof of correctness of an algorithm would be easier in a functional style of algorithm design than in an imperitve style.. However, how does one go about finding the efficiency of an algorithm written in a functional style? More on this later... (Go here for some Haskell related humor)