I don't understand why you think that immutable data structures are more difficult to reason about and prove properties of. Perhaps you would enlighten me.
Likely at least in part because they've been studied far less than mutable/imperative data structures, and thus there are significantly less tools for reasoning about them. Plus the most efficient functional datastctures rely on lazy evaluation, adding a layer of complexity to reasoning about their behavior. In fact, in his 10-years PFDS retrospective Okasaki noted exactly that:
> In 1993, I ran across an interesting paper by Tyng-Ruey Chuang and Benjamin Goldberg, showing how to implement efficient purely functional queues and double-ended queues. Their result was quite nice, but rather complicated, so I started looking for a simpler approach. Eventually, I came up a much simpler approach based on lazy evaluation, leading to my first paper in this area. (When I say simpler here, I mean simpler to implement—the new structure was actually harder to analyze than Chuang and Goldberg's.)
or
> , I went into a frenzy, playing with different variations, and a few hours later I came up with an approach again based on lazy evaluation. I was sure that this approach worked, but I had no idea how to prove it. (Again, this was a case where the implementation was simple, but the analysis was a bear.) [...] The whole way home I thought about nothing but how to analyze my data structure. I knew it had something to do with amortization, but the usual techniques of amortization weren't working.
That's the passage I was thinking of. Compare the implementation and analysis of queues in Purely Functional Data Structures with any introductory data structures book if you don't believe me.
