Class 2: LCF and HOL

This class talks about the foundations of the Isabelle/HOL proof assistant and similar proof assistants like HOL Light and HOL4, focusing on ephemeral proof objects (here described as the LCF architecture) and the underlying logic (HOL, a classical higher order logic based on the simply typed predicate calculus). There are three optional readings for the day: a blog post by Larry Paulson about the LCF architecture, a classic paper about LCF, and a later paper by Mike Gordon about the history of HOL and how it was derived from LCF.

This is the first of two classes exploring the foundations of some particular proof assistants. It looks at Isabelle/HOL, a popular proof assistant with ephemeral proof objects based on HOL. Isabelle itself is a system with a metalogic (logic for encoding logics) that supports reasoning in different logics; Isabelle/HOL instiatates this to HOL in particular.

Isabelle/HOL like other HOL variants (HOL Light and HOL4, for example) follows in the footsteps of LCF, a very early proof assistant. It keeps fairly closely to the original architecture of LCF. In the blog post, Larry describes the LCF architecture as a sort of alternative approach to the de Bruijn criterion when it comes to ensuring that proofs are correct, but I always view this as an alternative way of satisfying de Bruijn, where proofs can be reconstructed and checked, but where this is not necessary to do for correctness. We will cover this in class.

You can find a reading guide and some discussion questions below. Slides for the class are available here.

Readings this week are optional, but here are a few notes on each of the readings.

For the blog post by Larry Paulson, I think it's a really interesting take on the tradeoffs between ephemeral proof objects (the LCF architecture) and explicit proof objects (classic de Bruijn criterion). Since we discussed the tradeoffs of these a bit in class, it may be interesting to think about.

The classic LCF paper and the Mike Gordon paper about the evolution from LCF to HOL go well together. I recommend reading the classic LCF paper in just enough detail to get a sense of how proofs that use the LCF approach are correct by construction, and how automation interacts with that. Then the Mike Gordon paper is good for getting a sense of how LCF evolved into HOL, which is closely related to Isabelle/HOL and uses a similar logic and architecture (albeit without a metalogic that supports multiple different logics like the Isabelle system).

Note: The blog post contains a lot of opinions, and logicians and type theorists are often pretty opinionated about logic and type theory. I think it's important to remember that you can disagree wtih these opinions---we disagree with each other all the time. But it can be quite fun and enlightening to think about the reasons for and implications of holding these opinions. When it comes to foundations, though, there isn't really "right" and "wrong" (assuming some basic guarantees about the logic, like consistency when desirable)---there are only tradeoffs. But these tradeoffs are hugely consequential for what kinds of automation can be implemented, for how they can be implemented, for what can be expressed naturally in the logic, and for how a system ought to be designed, plus a whole lot more. So these conversations can get quite heated! Do not let that deter you from having them :).

Since the reading is optional, there is no need to post in the class forum thread, but feel free to do so if interested. Regardless, thinking about any one of these questions may help you better internalize the reading or lecture.

1. What about Larry Paulson's blog post do you agree with, and what do you disagree with? Does it change any of your thoughts on ephemeral versus explicit proof objects?
2. In the LCF approach, the trusted kernel is the definition of the thm abstract data type, and the interface for constructing a thm. Proofs are correct by construction because this interface is limited to the logical rules of the underlying logical system. What do you think it would take for you to understand and trust such a kernel? Do you understand the definition from the paper? If not, what is confusing to you, and does that impact how much you'd trust proofs done in such a system?
3. From what you've learned so far about the history of proof assistants derived from LCF, what would you consider in designing a modern proof assistant from scratch?
4. Write a paragraph responding to someone else's comment in the discussion forum.
5. Write a paragraph about any other single interesting thought, question, or idea that you had in response to the reading.