✳flâneur — a map of the web's best reading

"Why don't you use dependent types?"

lawrencecpaulson.github.io · 1,766 words · saved by 1 readers

To be fair, nobody asks me this exact question. But people have regularly asked why Isabelle dispenses with proof objects. The two questions are essentially the same, because proof objects are intrinsic to all the usual type theories. They are also completely unnecessary and a huge waste of space. As described in an earlier post, type checking in the implementation language (rather than in the logic) can ensure that only legitimate proof steps are executed. Robin Milner had this fundamental insight 50 years ago, giving us the LCF architecture with its proof kernel. But the best answer to the original question is simply this: I did use dependent types, for years. I was lucky enough to get some personal time with N G de Bruijn when he came to Caltech in 1977 to lecture about AUTOMATH. I never actually got to use this system. Back then, researchers used the nascent Internet (the ARPAnet) not to download software so much as to run software directly on the host computer, since most software

"Why don't you use dependent types?" Machine Logic At the junction of computation, logic and mathematics "Why don't you use dependent types?" 02 Nov 2025 [ memories AUTOMATH LCF Lean type theory Martin-Löf type theory NG de Bruijn ALEXANDRIA ] To be fair, nobody asks me this exact question. But people have regularly asked why Isabelle dispenses with proof objects. The two questions are essentially the same, because proof objects are intrinsic to all the usual type theories. They are also completely unnecessary and a huge waste of space. As described in an earlier post , type checking in the im

Explore this link on the map →

saved by

related reading