3 ms·

Are there downsides to the HOL approach when compared to constructive systems?

by bjz_ 10y ago

mafribe 10y ago
Depends what you want to do. If you are interested in program verification, then not all that much, because everything is about automation. Coq/Agda have a small edge if you want to prove something about Lambda calculus since Coq/Agda are themselves Lambda calculi, and not surprisingly most Coq/Agda work is about Lambda calculus ... The HOL school has probably a small edge in other areas. In practise the underlying approach (LCF vs Curry-Howard and dependent types vs HOL) makes much less of a difference than automation and availablility of proof libraries.
Retra 10y ago
It's hard to take something that's been proven true and turn it into something that's been proven useful without employing some constructive means.
- mafribe 10y ago
  I'm not sure I agree. For example CakeML [1] is the first fully verified self-hosting compiler for a substantial programming language, and seL4 [2] is the first fully verified substantial operating system kernel. Both were verified in LCF provers using HOL as a logic. Are you saying that the guarantees of correctness are not in themselves useful? [1] https://cakeml.org/ https://cakeml.org/ [2] https://sel4.systems https://sel4.systems
  - Retra 10y ago
    If I write a program X and tell you it was proven correct, do you know that X is useful? To know that a correct program is useful, you have to know what it does. And if you know what it does, you have constructed an implementation. Which is to say that a nonconstructive verifier is really just deferring the 'constructive' part of its operation to the compiler and programmer. (And this is the 'hard part' I was referring to.)
    - mafribe 10y ago
      I'm not sure what you mean. We are discussing the (dis)advantages of HOL vs constructive reasoning (e.g. Coq). The main difference is that HOL-based provers like Isabelle/HOL has classical built in from the start -- all proof automation supports classical reasoning. Constructive reasoning eschews classical methods. In order to prove the correctness of a program X, I need a specification S, and then I construct a proof P that X |= S, i.e. that X satisfies the specification S. I use an interactive proof assistant to check the proof P. There is no disadvantage that I can see if the proof P of X |= S is classical, at least from the point of view of program correctness. Maybe you mean something else?

Are there downsides to the HOL approach when compared to constructive systems?

by bjz_ 10y ago

Are there downsides to the HOL approach when compared to constructive systems?

Depends what you want to do. If you are interested in program verification, then not all that much, because everything is about automation. Coq/Agda have a small edge if you want to prove something about Lambda calculus since Coq/Agda are themselves Lambda calculi, and not surprisingly most Coq/Agda work is about Lambda calculus ... The HOL school has probably a small edge in other areas. In practise the underlying approach (LCF vs Curry-Howard and dependent types vs HOL) makes much less of a difference than automation and availablility of proof libraries.

Retra 10y ago

It's hard to take something that's been proven true and turn it into something that's been proven useful without employing some constructive means.

mafribe 10y ago
I'm not sure I agree. For example CakeML [1] is the first fully verified self-hosting compiler for a substantial programming language, and seL4 [2] is the first fully verified substantial operating system kernel. Both were verified in LCF provers using HOL as a logic. Are you saying that the guarantees of correctness are not in themselves useful? [1] https://cakeml.org/ https://cakeml.org/ [2] https://sel4.systems https://sel4.systems
- Retra 10y ago
  If I write a program X and tell you it was proven correct, do you know that X is useful? To know that a correct program is useful, you have to know what it does. And if you know what it does, you have constructed an implementation. Which is to say that a nonconstructive verifier is really just deferring the 'constructive' part of its operation to the compiler and programmer. (And this is the 'hard part' I was referring to.)
  - mafribe 10y ago
    I'm not sure what you mean. We are discussing the (dis)advantages of HOL vs constructive reasoning (e.g. Coq). The main difference is that HOL-based provers like Isabelle/HOL has classical built in from the start -- all proof automation supports classical reasoning. Constructive reasoning eschews classical methods. In order to prove the correctness of a program X, I need a specification S, and then I construct a proof P that X |= S, i.e. that X satisfies the specification S. I use an interactive proof assistant to check the proof P. There is no disadvantage that I can see if the proof P of X |= S is classical, at least from the point of view of program correctness. Maybe you mean something else?