I've read Godel, Escher, Bach, and I've read this. It's a very nice explanation.

But everywhere I see, Godel's theorem is touted as some kind of deep philosophical insight, whereas from what I understand, informally it could be rephrased as "if you have a usable language for mathematical proofs, some phrases in that language must be neither true nor false (i.e. nonsensical)".

Nonsensical phrases in our human languages in nothing new, so the conclusion becomes that much less exciting. Though I'm sure it's valuable for fundamental math theory.