Why don't you use dependent types?
Автор объясняет, что Isabelle сознательно отказалась от объектов доказательств, которые являются неотъемлемой частью обычных теорий типов. Это сделано потому, что объекты доказательств не нужны и занимают много места. Вместо этого Isabelle использует архитектуру LCF, где проверка типов осуществляется в языке реализации, а не в логике, что гарантирует легитимность шагов доказательства. Robin Milner имел это фундаментальное понимание 50 лет назад.
Лоуренс Полсон рассказывает о своем опыте работы с AUTOMATH и Martin-Löf type theory. Первоначально Isabelle была реализацией Martin-Löf type theory, которая до сих пор включена в дистрибутив как Isabelle/CTT. Однако автор переключился на более общий подход, вдохновленный AUTOMATH - "большим рестораном, который обслуживает любую кухню". В итоге Isabelle/HOL стала доминирующей, хотя де Брёйн не одобрял растущую мощь теорий типов и презирал теорию множеств.