[duve02]

> You could write this same proof in absolutely any language that supports recursion

Well, you at least need dependent types just to state the theorem, which eliminates nearly all other languages.