[Chattered]

Proof assistants are frequently used to prove the correctness of computer programs. And since a proof assistant is a computer program, and often quite a complex one that could contain bugs that render everything it does useless, you might want to use your proof assistant to prove that its code does what you hope it does.

Goedel's second incompleteness theorem says you can't do that. Ever. And more generally, it says that you will hit a roadblock as you try to prove what it is that your proof assistant does. This is really annoying.

But you can get pretty damn close. HOL Light has something of a self-consistency proof that is so close to the real thing that it's worth taking seriously.

But incompleteness, by itself, isn't a big deal for theorem provers. Russell himself worked as if the existence of infinities wasn't provable, which is why Goedel had little relevance to Russell. Hilbert on the other hand....