[Radle]

"And at the very bottom there is a base piece of theorem-proving software that is only a few hundred lines of code that has been validated only by humans and self tests."

Is it possible for that part of the system, to proof it's own correctness?

It's obvious that the danger with such a proof is that the code may think it's correct while it's incorrect in thinking it's correct.

But if I have learned one thing, then that Mathematicians can sometimes be really sly foxes.

[taktoa]

It could prove its own correctness, but there is still the possibility that it has a bug that causes its proof of correctness to be meaningless :-)