This post contains a cursory discussion of Gödel's incompleteness theorem and a promise to deliver on the title in a subsequent post.

Yes, this has all the hallmarks of the light intro post.

But it has the important take-away that is claiming (and I agree) that we shouldn't be too worried about the fact that some things can't be proven within formal systems. We have what amounts to a huge body of empirical experience that roots our confidence in many things, including set theory.

Indeed we have no real way of giving our stamp of approval to a formal system except by our intuitions about what reason is, as modified by our life experience. And even the innate intuitions are the product of biological evolution, which is another kind of empirical testing process.

The one time a blogger writes content that actually has me glued to the page, is the one time the blog is actually too short instead of way too long.

I'm curious... is it really true that an inconsistency would invalidate all proofs? Wouldn't this only affect non-constructive proofs (i.e., proofs that rely on the law of the excluded middle)? According to Wikipedia intuitionists also accept the principle of explosion... but it's not just an automatic result, is it? You'd need some proof or assumption that contradiction implies everything. Right?

In case you are wondering, it has nothing to do with the Go programming language.

It doesn't have anything to do with go, the game, either. Not yet. The part about games is for the next post which according to the author is very soon. Incompleteness of posts...

Can we prove this post is incomplete though?

Which is fantastic. Go gets IMHO a disproportionate amount of attention considering it takes 4 times as many lines of code to do what any functional language can do.