Isabelle's Design Philosophy: Why It Avoids Dependent Types and Proof Objects

Summary

This article discusses the design philosophy behind the Isabelle proof assistant, explaining why it doesn't use dependent types or proof objects like other type theories. The author argues that proof objects are unnecessary and wasteful, and that Isabelle's approach of type checking in the implementation language (rather than in the logic) is more efficient. The piece explores the historical context of proof assistants, comparing different systems and their approaches to formal verification.