The "proving theorems" stuff is definitely overstated. People always toss that term around, and it's true in principle, but in practice hardly anyone ever uses

The "proving theorems" stuff is definitely overstated. People always toss that term around, and it's true in principle, but in practice hardly anyone ever uses correctness proofs in real world code. But to flip it around and make a less grandiose version of the same point: the majority of bugs are to do with state. (I don't actually know if that has been "proved" but it's definitely what I find in practice!) Pure FP gets rid of a whole swathe of potential bugs at one stroke. Of course it makes programming harder in some other respects, as often it can be hard to figure out a pure function that's as efficient as the obvious imperative algorithm, or even to figure out how do a state-y thing in FP in the first place.