Interactive Theorem Proving, Guest Lecture – Introduction to HOL [video] | Hacker News Reader

Interactive Theorem Proving, Guest Lecture – Introduction to HOL [video]

youtube.com

52 pointsmatt_d10 comments

Isn’t HOL a bit oldfashioned now that we have Lean?

At 1:27, "So then, you can ask, why didn't [Apple and AWS] choose Coq, Lean or Agda [instead of Isabelle/HOL]?"

My understanding (having only used dependent-types -family interactive theorem provers) is that if your property can be expressed in HOL, proving it will require far less human effort to prove than Coq or similar.

Yes.

A lot of proof automation is based on SAT/SMT solvers like Z3, which are based on classical logic.

It is funny that Z3 was done by the Lean guy. But it probably also explains that Lean basically switched to classical logic.

There ist Jeremy Avigad's influence. He is not the typical type theorist and definitely no constructive zealot.

"I have been contributing to the development of the Lean Theorem Prover since its inception. I led the development of the first libraries and documentation.."

"Many parts of classical mathematics, however, have not been developed constructively."

https://www.andrew.cmu.edu/user/avigad/research.html

https://www.andrew.cmu.edu/user/avigad/Teaching/classical.pd...

Yes, I know him.

Related response [0] and [1]. It is a bit of a matter of taste: I prefer classic stuff as I have used that for decades. HOL is ‘easy’, but I haven’t spent as much time with Lean.

[0] https://news.ycombinator.com/item?id=14744167

[1] https://news.ycombinator.com/item?id=25061513

HOL is a classical (i.e. non-constructive) logic based on simple type theory, and that makes proof automation much easier. Adapting the kind of proof automation that classical logic with simple types enables to a Curry-Howard based prover with dependent types (like Lean, Coq or Adga) is not a fully solved problem.

For industrial-scale program verification, proof automation is everything! Nothing else matters.

I conjecture, but don't know, that Amazon write their HOL-based prover from scratch, to take into account their cloud resources. So it might well be the most modern prover of all.

Note that Leonardo de Moura, who initiated Lean, is now at AWS. To add even more complications, AWS does also use Lean, e.g. https://github.com/leanprover/SampCert

Do Amazon actually write their own HOL-based prover from scratch?

I don't know, but given that AWS has 1000s if note millions of servers that may have idle cycles, it makes sense to use them for automatic theorem proving. And there is no existing ITP or even SMT solver that was specifically designed for efficient use of so much parallelism.

AWS certainly hired a lot of senior STM and ITP guys, such as John Harrison.

Reply on news.ycombinator.com