"In Gödel's case, the really deep insight was that types can't protect a formal system against the incompleteness/inconsistency problem because types, unless they actually cripple the power of the system, can only prevent the system from acknowledging that it has a problem, they don't prevent the problem from being there."