I would not recommend believing anything Roger Penrose ever said about computation and/or Godel. His entire book "Emperor's new mind" was insane garbage at the core. Penrose has at various times been brilliant but that book was not it. Here's a fact. A universal turing machine (UTM) is capable of running a program P which will prove that its design indeed represents a UTM. This proof will be valid no matter what input that UTM ever might have. Further, said program P can be proven to be correct, and a verification of said proof could be performed by P itself. (P would be a "verified general-purpose proof-verifier.") This proof will be valid no matter what input might later be given to program P. I suspect that programs of this "self proving" ilk might become important, or even essential, in the future. But right now, most programs are unproven barf, and large programs contain many bugs. And even if self-proving programs become commonplace, that will be no means be a cure-all.