Re: [isabelle] Syntax issue: lost between HOL and Isar

I've been totally focused on the frontend languages, ML, Isar, and HOL, while knowing nothing about what the backend prover does with them.

I now have a way to make sense of it all being Isar syntax, the HOL syntax being a part of the Isar syntax, and HOL not being dependent on Isar.

It could be that Isar is a framework that HOL uses to state lambda calculus terms, and the backend strips away all the outer syntax, where all that's left is the HOL lambda calculus terms. That idea lines up with Christian saying that proofs are irrelevant.

Now I sit on the two ideas and wait to see if I read something that supports one of the two ideas, that HOL inherits Isar and makes it its own, or Isar is a framework that gets stripped away by the backend. Today, right now, I'm leaning towards the idea that much of the Isar gets stripped away.

(I do see "framework" in "Chapter 2 The Isabelle/Isar Framework", which is where I must have gotten "framework". I don't see "stripped away" anywhere yet. There's a lot I haven't read yet.)

I don't really care to know the details of what the backend does, it would take years to learn about it, but it's nice to make sense of important high-level concepts.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.