3 ms·

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

remexre 2y ago
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.
- GregarianChild 2y ago
  Yes. A lot of proof automation is based on SAT/SMT solvers like Z3, which are based on classical logic.
  - auggierose 2y ago
    It is funny that Z3 was done by the Lean guy. But it probably also explains that Lean basically switched to classical logic.
    - hackandthink 2y ago
      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/research.html https://www.andrew.cmu.edu/user/avigad/Teaching/classical.pdf https://www.andrew.cmu.edu/user/avigad/Teaching/classical.pd...
      - auggierose 2y ago
        Yes, I know him.
anonzzzies 2y ago
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 https://news.ycombinator.com/item?id=14744167 [1] https://news.ycombinator.com/item?id=25061513 https://news.ycombinator.com/item?id=25061513
GregarianChild 2y ago
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 https://github.com/leanprover/SampCert
- auggierose 2y ago
  Do Amazon actually write their own HOL-based prover from scratch?
  - GregarianChild 2y ago
    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.

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.

GregarianChild 2y ago
Yes. A lot of proof automation is based on SAT/SMT solvers like Z3, which are based on classical logic.
- auggierose 2y ago
  It is funny that Z3 was done by the Lean guy. But it probably also explains that Lean basically switched to classical logic.
  - hackandthink 2y ago
    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/research.html https://www.andrew.cmu.edu/user/avigad/Teaching/classical.pdf https://www.andrew.cmu.edu/user/avigad/Teaching/classical.pd...
    - auggierose 2y ago
      Yes, I know him.

anonzzzies 2y ago

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 https://news.ycombinator.com/item?id=14744167 [1] https://news.ycombinator.com/item?id=25061513 https://news.ycombinator.com/item?id=25061513

GregarianChild 2y ago

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 https://github.com/leanprover/SampCert

auggierose 2y ago
Do Amazon actually write their own HOL-based prover from scratch?
- GregarianChild 2y ago
  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.