[plt-scheme] The perfect teaching language--Is this too much to ask for?
> I guess it's analogous to the problem with "the set of all sets" that
> led to Russell's paradox, the dismantling of naive set theory, the
> _Principia Mathematica_, and thence to Goedel's incompleteness theorems.
I'd like to see some more dots connected.
While Russell & Whitehead's theory to avoid the paradox involved a
hierarchy, the set theories that were widely embraced (eg Zermelo-Fraenkel
and von_Neumann-Bernays-Goedel) had little or no hierarchy.
> I'll have to think about this: "type" as a type still seems so elegant,
> so expressively efficient. ... Has somebody already proven that that's
> unattainable too?
While Meyer and Reinhold's paper is suggestive, it doesn't appear to me to
be the last word. We want to avoid a system that can prove "bad"
theorems. Might there be other ways to avoid bad theorems other than
hierarchy?
-Arthur