I'm not sure why pier25 was reminded, but Russell's type theory and Gödel's incompleteness theorem are closely related. They both arose in response to the foundational crisis in mathematics [1].
Russell stumbled onto Russell's paradox (among others) and it shook mathematicians' confidence that everything in math was built on top of a perfectly consistent and stable foundation. If you can define a set that it "the set of sets that don't contain themself" then what other kind of crazy talk can you say in math? How do you know proven things are true and false things can't be proven in the face of weirdness like that?
Russell tried to solve the problem by inventing type theory. Types stratify the universe of values such that "the set of sets that don't contain themself" is no longer a valid statement to make.
Meanwhile, Gödel went and proved that, sorry, no, math is not consistent and complete. There are statements that are true but which cannot be proven.
> Similarly, type theory wasn’t enough to describe new foundations for mathematics from which all mathematical truths could in principle be proven using symbolic logic. It wasn’t enough because this goal in its full extent is unattainable.
I spent the whole article wondering when Gödel would be mentioned, and was disappointed that he wasn't given that the Incompleteness Theorem was at least partly a response to Russell's work, and because it applies directly to computer systems. The conclusions Gödel reached are asserted in the article but not cited which is weird given the other references.
I was reminded of Godel too. For me, it was the part of the article that described Russell's finding of statements that led to paradox, such as "I am lying." If you're allowed to talk about "the set of all sets", then you can state things that can't be dealt with logically. That reminds me of Godel's Incompleteness theorem.
For one, Godel used the same kind of self-referential statements described in the article ("this proposition is not provable" etc) and used math to create a kind of enumeration of propositions and have the proposition refer to itself.
