Slightly off-topic but after reading Douglas Hofstadter's books the one thing that I never managed to grok was Godel's incompleteness theorem. It's implications are fascinating but my math background never allowed me to completely understand it's proof.

 Pick some formal system X which can handle basic arithmetic. The basic idea is to take the classic paradox, "This sentence is false," and embed it into maths. The sentence actually constructed is something like, "This theorem is not provable within formal system X," and it's phrased as a theorem of formal system X.The main ingredient we need here is to realize that numbers can represent sentences in formal systems. This should be obvious to computer scientists of today, but it was ground-breaking at the time.Another thing we'll need is diagonalization. Some folks get hung up on this one; ultimately, you'll have to convince yourself that it's a valid technique.Hofstadter's explanations, both the long gentle one in GEB and the quick fuzzy one in "I Am A Strange Loop", are much more detailed and correct on this, so I'd advise going back and making sure you understand each step.Also, something that doesn't get enough airtime is Tarski's Undefinability, which says that a formal system afflicted by incompleteness is not capable of talking about truth in certain basic and important ways which would enable a formal system to fully represent itself.
 I'd highly recommend "Gödel's Proof" by Ernest Nagel and James Newman (https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/081...). It'll probably require a bit of patience to go through, but should be fairly accessible to reader without an extensive mathematics background.
 Whole-heartedly seconded. I went through the proof twice, once in a math context and once a philosophical one. This work was referenced in both.
 What are the practical implications of the incompleteness theorem?
 Mathematics is postmodern; there's no single formal system which is the concrete bedrock of mathematics, and there will always be some true-but-unprovable theorems in consistent formal systems.Cynics might take this to mean that maths is meaningless. On the contrary, I'd like to suggest that maths is the canonical emergent pattern; any formal system with sufficient complexity to represent itself will automatically exhibit some algebraic structure, and maths emerges naturally from there.The biggest implication for computer scientists is that, combined with results of Church and Tarski, we should expect that meta-languages are more powerful than object-languages, whether this is by preprocessing and macros like in C/C++ and CL, or by avoiding using meta-features except when necessary like in Python and Ruby.
 There will always be more math to be discovered, because there will always be theorems you can state but not prove within the confines of the existing systems.
 You cannot ever know for sure that your software is bug free, because no finite system of logic is both true and complete.At least, that’s my understanding of it.
 Not exactly.For any sufficiently powerful system (Turing completeness is definitely powerful enough) there are statements which are true but cannot be proven by that system. Secondarily, no system can demonstrate its own consistency.However, if you limit your software enough, you can prove that every possible input is handled correctly. That involves removing Turing completeness. E.g. once you accept a language as a configurator, you can no longer prove that. CSS3 is Turing complete. JSON is not.One requirement is limiting the size of inputs.
 Afaik this is all related to relativity. No good or bad unless unrelated like ++ or -- and we're in a system where, at least humans, only perceive reality as it relates to us. You need air, so do I, together we have a similar need but also together we occupy each other's space and resource
 This is a good lecture from CMUs 15-251 class on his two incompleteness theorems https://youtu.be/bmECBK_TOQA

Search: