For some values of "pure", sure. The problem is, keeping this level of purity - that allows to strictly prove theorems about your code - is very hard. And most real code would compromise, while still pretending that they are pure and their results are proven. That's not a road to a good place.
I seriously doubt there's much industrial code made in functional languages that has been proven to be correct. And I'm not talking about halting problem, etc., not that deep, I mean just writing a spec of what the code would do in every situation and proving that indeed it does that. I haven't seen any. Maybe in theory it'd be possible, in practice, it doesn't happen. In fact, if that happened frequently, unit testing in functional environments would not exist - you don't need to test what you can prove to be correct. In reality, it very well exists.
> There is a reason why the majority of proof assistants are implemented as functional languages.
It's not the direction you need to prove though. Surely, it is easier to express things we can prove in functional terms. The challenge, however, is to see if it's easy to prove
that code follows certain specs when that spec is not specially fit for being expressed in functional terms.
> it's that what's new about it (privileging the first argument of each procedure, inheritance, lots of hidden mutable state) is bad
Hidden mutable state is not mandated by OOP in any way. And arguing that inheritance and special arguments are bad would require some more than just saying "it's bad".
> and what's good about it (encapsulation, polymorphism) is not new
So what? Where's the problem if it's not new? Letters we're using aren't new, so aren't numbers, still serve us well. Not everything good must be new, if it's old and still good - even better. I fail to see how "it's not new" is any meaningful criticism - it's like criticizing a math library that the result it returns for 2+2 is not new. Why would we want it to be new?