His incompleteness theorems meant there can be no mathematical theory of everything, no unification of what’s provable and what’s true. What mathematicians can prove depends on their starting assumptions, not on any fundamental ground truth from which all answers spring.

If all this talk of substitution and self-reference remind you of programming, recursion, or lambda calculus, have a look at Incompleteness Ex Machina:

In this essay we'll prove Gödel's incompleteness theorems twice. First, we'll prove them the good old-fashioned way. Then we'll repeat the feat in the setting of computation. In the process we'll discover that Gödel's work, rightly viewed, needs to be split into two parts: the transport of computation into the arena of arithmetic on the one hand and the actual incompleteness theorems on the other. After we're done there will be cake.

As someone who is quite interested in formal methods (briefly: the application of mathematics and proofs to "real-world" systems), understanding Gödel's and Tarski's incompleteness theorems was an existential moment for me. They underpin a lot of my current ideas about what "factual truth" is and the limitations of mathematics and modeling techniques. For those very curious, this has applications to physics models and simulations as well: Fundamental Limits of Cyber-Physical Systems Modeling touches on some undecidable issues when constructing even very simple models of systems.