5 ms·

A note for the unitiated: There is a tension between TLA+ and Coq et al. (typified by statements such as "weird computer-science math") that is similar and mayb

by nmrm2 11y ago

A note for the unitiated: There is a tension between TLA+ and Coq et al. (typified by statements such as "weird computer-science math") that is similar and maybe even rooted in to the sorts of culture wars that sprout up around programming languages (see [2] of parent's post for a perfect example of what I'm talking about...) The characterization in pron's post is decidedly biased toward TLA+ in a way that I think is unnecessary. A few correctives: * Coq has seen plenty of industry adoption. To say that type-theoretic theorem provers (or the Coq system specifically) are merely academic toys compared to TLA+ is wrong. * "Normal" mathematicians (not just "weird Computer Science-type" mathematicians, whatever that means...) have used and extolled the virtues of Coq as a tool as well as its theoretical foundations. See e.g., the univalent foundations project. Regardless, I'm not sure I understand why "Computer Science-type math" is an unreasonable foundations for a program specification tool, which is what TLA+ is. And if the goal is formalized mathematics, you're probably better off with Coq (and it's not even clear that the TLA+ community is interested in that sort of thing, independnet of results useful in the course of a program specification/verification task.) * If you're familiar with (esp. typed) functional programming, you might find Coq even easier to get into than TLA+. On both sides of the type theory vs sets/axioms divide, people should be careful not to confuse one's predispositions based upon educational background with the actual mental load of learning to use a tool. There is room for both of these tools (and more!) in the world. I don't understand why they have to be in competition. A formalization of the C standard is a HUGE undertaking, independent of what tool was used. Let's celebrate that achievement!

unboxed_type 11y ago
I would like to mention that Coq is also used to extract _verified implementations_ rather than model checking abstract algorithm design (as in TLA+). This property might be very desirable depending on situation. As for me this property looks very appealing.
pron 11y ago
> To say that type-theoretic theorem provers (or the Coq system specifically) are merely academic toys compared to TLA+ is disingenious. I never said that Coq is an academic toy. Some projects done in academia and used in the industry have been verified with Coq, but I am not aware of actual (direct) use of Coq in the industry (but would be interested to learn of any). > I'm not sure I understand why "Computer Science-type math" is an unreasonable foundations for a program specification tool, which is what TLA+ is I've never said it is unreasonable, only that it is foreign to most engineers (as well as most academic CS people), or rather, more foreign than basic logic/set theory. I would say again that if you're comfortable with type theory, you might enjoy Coq better. If not, TLA+ would probably be more approachable. TLA+ has the added advantage of having a model checker, which is very useful when you don't have the resources required for a full proof, but still want a good confidence in the correctness of your algorithm. > A formalization of the C standard is a HUGE undertaking, independent of what tool was used. Let's celebrate that achievement! Oh, absolutely! It's just that stories like this make people interested in formal methods, and Coq, IMO, would be daunting for most. TLA+ is a good entry point to formal methods, even if you later choose to move to dependent-type approaches and tools.
- yaantc 11y ago
  > ... but I am not aware of actual (direct) use of Coq in the industry (but would be interested to learn of any). The first EAL7 certified smart card certification used coq, see: https://www.commoncriteriaportal.org/iccc/9iccc/pdf/B2404.pdf https://www.commoncriteriaportal.org/iccc/9iccc/pdf/B2404.pd...
  - pron 11y ago
    Oh, wow, they have verified a (JavaCard) JVM. Impressive! Thanks. They mention > 117,000 lines of Coq with > 1600 proofs to get EAL7 for the JVM.
  - brohee 11y ago
    This link is about an EAL4+ evaluation
    - wolfgke 11y ago
      If you read slide 4, you'll see that the SIM card was evaluated at EAL4+ level and the design of the Java Card System at EAL7 level.
pron 11y ago
BTW, what is the justification for using dependent type rather than stating assumptions/theorems directly in predicate logic over set theory (as in TLA+)? Lamport has this to say on the matter: The main virtue of these type theories is precisely that they are constructive. A constructive proof that two arbitrary numbers always have a greatest common divisor provides an algorithm for computing it [Thompson 1991]. Researchers, using tools such as Coq and Nuprl are investigating whether this can lead to a practical method of synthesizing programs. You can perform classical reasoning in a constructive type theory by adding P ∨ ¬P as an axiom. The resulting system will probably be strong enough to handle any specification problem likely to arise. However, it will be no stronger than ZF, and it will be much more cumbersome to use. In the end, he opted for set theory because it is simpler, more familiar, and more flexible. Are there any advantages to using dependent types? Is the main advantage indeed synthesizing programs from proofs?
- pacala 11y ago
  FWIW, https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Mizar_system is based on set theory, and has traction in the math community.
- nmrm2 11y ago
  > Is the main advantage indeed synthesizing programs from proofs? It's one major advantage, yes. And not just for the sake of software verification. Sometimes when proving a non-CS-type-math theorem you still want an efficient implementation of an existence proof. But code synthesis is a lot harder than merely being constructive, and efficient code synthesis even more so. Use cases for Coq that depend upon code synthesis don't come for free just by avoiding LEM. So although it's fair to say that you can do classical reasoning in Coq, I'm not sure saying you can do synthesis from TLA+ if only you avoid LEM is fair at the moment (I might be wrong). > Are there any advantages to using dependent types? Here are a few other reasons for using Coq: * Proof terms. There are two major disagreements here. The first grounds out in philosophy and the second basically amounts to "you really want to compose the proofs and make sure they are still a proof instead of just throwing away the proof and using the theorem" which has lots of good systems-y justifications * Specifically wrt TLA+, Modus Operandi matters. If you want a formal proof in the typical sense of the word (rather than a verification of fact based upon model checker output), then Coq userlands's tactics and theorems are useful. * Lots of people like to disparage the amount of algebra that FPers talk about. But it turns out that if studying those algebraic structures is your day job, the relationships between types and algebraic structures makes type theory convienant. >simpler, more familiar This is almost definitionally subjective. Which isn't meant as a criticism, in-so-far as one realizes that other people might have different experiences and so might (just as validly) consider other formalisms more familiar. > and more flexible There are (obviously) a lot of people who fundamentally disagree with the concrete arguments Lamport makes in this paper. I wish someone would annotate the paper with references to literature from the type theory community that address some of his concerns. For the record, I don't disagree with Lamport. I think Lamport is right -- for some use cases, it certainly makes sense to stick with ZF. But he's also wrong -- sometimes, the type theoretic approach really is simpler, more familiar, and more flexible. E.g., in the case of this dissertation.

by nmrm2 11y ago

unboxed_type 11y ago

I would like to mention that Coq is also used to extract _verified implementations_ rather than model checking abstract algorithm design (as in TLA+). This property might be very desirable depending on situation. As for me this property looks very appealing.

pron 11y ago

> To say that type-theoretic theorem provers (or the Coq system specifically) are merely academic toys compared to TLA+ is disingenious. I never said that Coq is an academic toy. Some projects done in academia and used in the industry have been verified with Coq, but I am not aware of actual (direct) use of Coq in the industry (but would be interested to learn of any). > I'm not sure I understand why "Computer Science-type math" is an unreasonable foundations for a program specification tool, which is what TLA+ is I've never said it is unreasonable, only that it is foreign to most engineers (as well as most academic CS people), or rather, more foreign than basic logic/set theory. I would say again that if you're comfortable with type theory, you might enjoy Coq better. If not, TLA+ would probably be more approachable. TLA+ has the added advantage of having a model checker, which is very useful when you don't have the resources required for a full proof, but still want a good confidence in the correctness of your algorithm. > A formalization of the C standard is a HUGE undertaking, independent of what tool was used. Let's celebrate that achievement! Oh, absolutely! It's just that stories like this make people interested in formal methods, and Coq, IMO, would be daunting for most. TLA+ is a good entry point to formal methods, even if you later choose to move to dependent-type approaches and tools.

yaantc 11y ago
> ... but I am not aware of actual (direct) use of Coq in the industry (but would be interested to learn of any). The first EAL7 certified smart card certification used coq, see: https://www.commoncriteriaportal.org/iccc/9iccc/pdf/B2404.pdf https://www.commoncriteriaportal.org/iccc/9iccc/pdf/B2404.pd...
- pron 11y ago
  Oh, wow, they have verified a (JavaCard) JVM. Impressive! Thanks. They mention > 117,000 lines of Coq with > 1600 proofs to get EAL7 for the JVM.
- brohee 11y ago
  This link is about an EAL4+ evaluation
  - wolfgke 11y ago
    If you read slide 4, you'll see that the SIM card was evaluated at EAL4+ level and the design of the Java Card System at EAL7 level.

pron 11y ago

BTW, what is the justification for using dependent type rather than stating assumptions/theorems directly in predicate logic over set theory (as in TLA+)? Lamport has this to say on the matter: The main virtue of these type theories is precisely that they are constructive. A constructive proof that two arbitrary numbers always have a greatest common divisor provides an algorithm for computing it [Thompson 1991]. Researchers, using tools such as Coq and Nuprl are investigating whether this can lead to a practical method of synthesizing programs. You can perform classical reasoning in a constructive type theory by adding P ∨ ¬P as an axiom. The resulting system will probably be strong enough to handle any specification problem likely to arise. However, it will be no stronger than ZF, and it will be much more cumbersome to use. In the end, he opted for set theory because it is simpler, more familiar, and more flexible. Are there any advantages to using dependent types? Is the main advantage indeed synthesizing programs from proofs?

pacala 11y ago
FWIW, https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Mizar_system is based on set theory, and has traction in the math community.
nmrm2 11y ago
> Is the main advantage indeed synthesizing programs from proofs? It's one major advantage, yes. And not just for the sake of software verification. Sometimes when proving a non-CS-type-math theorem you still want an efficient implementation of an existence proof. But code synthesis is a lot harder than merely being constructive, and efficient code synthesis even more so. Use cases for Coq that depend upon code synthesis don't come for free just by avoiding LEM. So although it's fair to say that you can do classical reasoning in Coq, I'm not sure saying you can do synthesis from TLA+ if only you avoid LEM is fair at the moment (I might be wrong). > Are there any advantages to using dependent types? Here are a few other reasons for using Coq: * Proof terms. There are two major disagreements here. The first grounds out in philosophy and the second basically amounts to "you really want to compose the proofs and make sure they are still a proof instead of just throwing away the proof and using the theorem" which has lots of good systems-y justifications * Specifically wrt TLA+, Modus Operandi matters. If you want a formal proof in the typical sense of the word (rather than a verification of fact based upon model checker output), then Coq userlands's tactics and theorems are useful. * Lots of people like to disparage the amount of algebra that FPers talk about. But it turns out that if studying those algebraic structures is your day job, the relationships between types and algebraic structures makes type theory convienant. >simpler, more familiar This is almost definitionally subjective. Which isn't meant as a criticism, in-so-far as one realizes that other people might have different experiences and so might (just as validly) consider other formalisms more familiar. > and more flexible There are (obviously) a lot of people who fundamentally disagree with the concrete arguments Lamport makes in this paper. I wish someone would annotate the paper with references to literature from the type theory community that address some of his concerns. For the record, I don't disagree with Lamport. I think Lamport is right -- for some use cases, it certainly makes sense to stick with ZF. But he's also wrong -- sometimes, the type theoretic approach really is simpler, more familiar, and more flexible. E.g., in the case of this dissertation.