He shows this by demonstrating a particular technique that can look at any formal system and build a statement that breaks it. Hence, any proof checker will have statements it can't handle.

He shows that for any given proof system, there exist statements for which no proof exists and no disproof exists either. That is not the same as breaking the proof-checker, which only cares about the particular proof it's given, not about whether other proofs or disproofs exist.

Proof generation is inherently complex. Proof verification is nearly trivial, and very well understood.

Hence, any proof checker will have statements it can't handle.

There are many things wrong with many of your statements here, but this one is particularly simple. You simply misunderstand what a proof checker does.

A proof checker does not deal with statements, it deals with formal proofs. Proof checking is roughly as complicated as parsing a context free language. That is, it is almost a trivial task.

Proof finding is another matter. A proof finder (aka a "theorem prover") takes a statement as input and attempts to produce a proof as output. Godel shows that there are statements that a proof finder can't handle.

You have repeatedly made claims which only make sense if you have the two kinds of programs confused. Fix that confusion, please.

Colloquially, Godel's theorem says that for any formal system complex enough to implement a certain subset of mathematics there will be syntactically valid theorems that the system cannot evaluate. He shows this by demonstrating a particular technique that can look at any formal system and build a statement that breaks it. Hence, any proof checker will have statements it can't handle.

There's a lot to object to there, but let's be generous about "colloquially." Here is a more precise and correct rewording of your last line: "Any algorithm that takes a statement as input and searches for a proof or disproof will fail on some inputs." Here is a more precise and incorrect rewording: "There is no algorithm that takes a proof as input and evaluates the correctness or incorrectness of that proof."

Now, some people concede that much, but insist that it doesn’t matter because Godel statements are just an oddity they can hard-code their systems to ignore.

I dare you to find someone actually claiming that (preferably someone making the claim under his real name, as a low barrier for eliminating clueless idiots on forums and comment threads.)

When such a system encounters a statement it can’t evaluate it might ignore it, or hang, or crash, or break the stack and execute your malware as root –there’s no way to tell without specifically looking at (and testing) each different class of problematic statement the system could encounter.

Actually, type theory is poweful enough to prove that programs will never do any of these things, for all statements at once. People rarely bother to prove that their programs are correct, but only because it's not usually worth the effort.