I love the story of Jacob's ladder. Someone I respect quite a lot used it as an analogy for the modern struggle to build a universal type system that is both consistent and capable of operating without any axioms - e.g. being able to specify induction in the same language that you hope to use induction.