alt Hacker NewsI added proof objects ages ago to HOL Light, it is not a big deal. It's just, as Larry said, why would you want them in the first place?
I added proof objects ages ago to HOL Light, it is not a big deal. It's just, as Larry said, why would you want them in the first place?
In HOL Light? Just so you can run the proof objects through another prover like Isabelle. Wasn't that your original ambition?
As you know, Rocq and Lean folk want more than just that from their proof objects. They want proofs to contain executable code, often of the very programs they were verifying, and so treat their proof assistants like programming languages with verifiers attached. So you get complex recursion and inductive definitions baked into the kernel. Whether this is a good idea or not is obviously pretty disputed among us, though I'm mostly with you and Larry :)