Any sufficiently complicated mathematical proof contains an ad hoc, informally-specified, bug-ridden, inflexible implementation of half of type theory.