[Tainnor]

I think you have to be really, really charitable not to see the Second Incompleteness Theorem as a complete repudiation of the Hilbert Program - at least it destroys the possibility of proving ZFC consistent in PA - to the point that I think it's a reasonable simplification to say that the Hilbert program failed, even if the paragraph you linked shows that some people have been trying to salvage Hilbert's program by relaxing it a little. I'm aware e.g. of Gentzen's proof of the consistency of PA, but I don't find it plausible to claim that it uses "finitary methods". At the very least, I don't think such arguments would have convinced the people that Hilbert was trying to convince, such as intuitionists.

Your second point also seems like a very minor nitpick. Clearly, set theory is inconsistent if you don't impose any restrictions on what kinds of set can be formed (something that Cantor to my knowledge didn't do), which is what Russell's paradox showed. The fact that they used Frege's formalisation for setting up the paradox doesn't seem particularly relevant to me.