I'm here to tell you a dirty secret about Gödel's incompleteness theorems, after having been asked whether we might hit a "Gödel limit" when trying to prove the correctness of computer programs. My qualification to speak on this is that I'm a software engineer who used to be a mathematician with a strong interest in foundational logic and mathematical philosophy, and I still track the field. Here's the skinny about Gödel limits... Gödel's incompleteness theorems are theoretically and philosophically tremendously important, but most mathematicians don't expect the limits implied by those theorems to be important in practice - not at the proof scales accessible by humans. We don't know for sure, but the intuitive sense of most mathematicians is that true but Gödel-inaccessible theorems are probably far away from us in very weird corners of the space of all formally possible propositions. The reason for this intuition is that you have to do very odd contortions to construct a proposition that demonstrates Gödel-inaccessibility. Such constructions are not mathematically natural questions. Consider the contrast with the Continuum Hypothesis or the Axiom of Choice. These arise from very simple and natural questions the answers to which turn out to be unprovable in standard set theory. They are not weird, twisted constructions made specifically to force the axiom system to rupture something. Because all reasoning about computer programs is reasoning about finite sets, it seems highly unlikely that being able to prove the correctness of a program will ever depend on even unprovable propositions as natural as CH or AC, which are axioms about what you can do with infinite sets. Still less likely does it seem that the proof of any program will ever depend on a proposition that is Gödel-inaccessible. So, in practice, it is not worth worrying about Gödel-inaccessibility of program proofs. Unless you're the sort of person who worries compulsively about, oh, I dunno, being beaned by a meteorite made of solid platinum, in which case there probably isn't much I can do to ease your tension. Of course, we could be wrong. There could be a landmine, or any number of landmines, in the regions of proof space we care about. The real worry about the Riemann hypothesis isn't whether it's true or false, but that it might turn out to be such a landmine. Then again, the Riemann hypothesis involves claims about infinities. Even if it does turn out to be Gödel-inaccessible (and the most mathematicians don't worry that it is) it would be quite a bit more shocking if a proof on finite sets turned out to be.