Russell's paradox, as usually stated, doesn't actually prove anything, because it's usually given as a statement in English about set theory.

It is presented that way to make a point that naive set theory isn't workable.

I don't know whether Russell originally stated it in mathematical terms, in which case it would prove something. I've read numerous accounts of it, yet never seen > a mathematical presentation. Google fails me at present

It is presented rigorously in most intro set theory text books. In ZFC or any other standard set of set theory axioms, Russell's paradox ceases to be a paradox and the logic is instead a theorem of the form "For any set A, there exists a set B such B is not an element of A."

I don't count a statement of the form "x such that x is not a member of x" as mathematical, because my intuition doesn't want me to talk about sets being members of themselves unless I have a mathematical formalism for sets and set > membership for which that works. It's also not happy about the quantification of x in that sentence; it's a recursive quantification. Let's put it this way: Any computer program I have ever written to handle quantification would crash or loop forever if you tried to give it such a statement.

Well, a standard formalism (again such as ZFC) is perfectly happy talking about sets that recur on themselves this way. Indeed, it is actually difficult to make a system of set theory that doesn't allow you to at least talk about sets like this.

I'm curious, do you consider Cantor's diagnolization argument to be too recursive? What about Turing's Halting Theorem?