Of all the incompleteness-style theorems, I find the Halting problem to be the most approachable and also the most interesting. Maybe it's because I'm a software dev that dabbles in math rather than the other way around. But that makes me wonder if all of Gödel's theorems can be stated if 'software form', so to speak.
Also check out https://en.wikipedia.org/wiki/Rice%27s_theorem
basically generalized the halting problem to arbitrary semantic properties.
Right, if you're a software engineer, the realization that the two theorems are nearly-equivalent really takes the air out of a lot of the existential philosophizing around Gödel's incompleteness.
Gödel's argument basically says that any system of mathematics powerful enough to implement basic arithmetic is a computer. This shouldn't be surprising to software engineers because the equivalency between Boolean logic and arithmetic is easy to show. And if you have a computer, you can build algorithms whose outcome can't be programmatically decided by other algorithms.