Gödel proved that within any formal system sufficiently powerful to include ordinary arithmetic, there will always be undecidable statements that cannot be proved true, yet cannot be proved false.

Turing proved that within any formal (or mechanical) system, not only are there functions that can be given a finite description yet cannot be computed by any finite machine in a finite amount of time, but there is no definite method to distinguish computable from noncomputable functions in advance. That’s the bad news.

The good news is that, as Leibniz suggested, we appear to live in the best of all possible worlds, where the computable functions make life predictable enough to be survivable, while the noncomputable functions make life (and mathematical truth) unpredictable enough to remain interesting, no matter how far computers continue to advance.

from Turing’s Cathedral: The Origins of the Digital Universe by George Dyson