5 ms·

> 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

by 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.

ScottBurson 11y ago
I'm guessing LEM = Law of the Excluded Middle.
- nmrm2 11y ago
  Yes.
pron 11y ago
> 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. TLA+ has them, too. > in-so-far as one realizes that other people might have different experiences and so might (just as validly) consider other formalisms more familiar. So you think some people are more familiar with type theory than with undergrad-level set theory (ZF)? > sometimes, the type theoretic approach really is simpler, more familiar, and more flexible. E.g., in the case of this dissertation I don't see it (probably because my type theory is very, very basic; I'm an algorithm's guy and the thought that a data-structure of mine might need type theory to be specified makes me shudder), as in I fail to see anything that isn't readily expressible in simple classical logic + temporal logic. Could you explain?
- nmrm2 11y ago
  > TLA+ has them, too. Like I said, modus operandi matters. If I have to perform another model checking routine (possibly on an infinite state space) to slightly generalize a theorem, then in many cases that means I never really had a useful proof of it in the first place. Also, Coq's mathematics library is extensive and often closely follows the proofs found in graduate mathematics text books. Last I looked into TLA+, it was squarely focused on algorithms and hardware (not even CS-related mathematics more generally -- specifically algorithms and hardware). > So you think some people are more familiar with type theory than with undergrad-level set theory (ZF)? Do I think there exists some population of people who are "more familiar" with type theory than with ZF? Yes, starting, for example, with every researcher whose primary area of study is type theory. In fact, I think that anyone who doesn't honestly believe there are such people must have an extremely low opinion of quite a number of very smart people. (Also, set theory qua set theory gets really disgusting and kludgey really quickly, and is something that almost no undergraduate (or even phd student) is exposed to these days. The "set theory" you see in a discrete math course kind of barely scrapes definitions. I think most people who posit that "set theory" is nice and simple must've never really dove deem into the actual theory of set theory...) (Also, most real math these days quickly abstracts away from germanely set theoretic constructions. Mathematicians don't work in ZF. They do not. Most will tell you they do not, if they even know what ZF is. Which a lot won't, because their undergrad discrete math course is probably the last time they saw a truly formal derivation. And the mathematicians who do know what ZF is often can't regurgitate an axiomatization of ZF. If you tell a mathematician that all of math is just set theory, most will chuckle and wink and say "why, yes, yes it is", and hopefully you're in on the joke...) > I don't see it... I fail to see anything that isn't readily expressible in simple classical logic + temporal logic. Could you explain? Did you read this dissertation's explanation of why separation logic is important? To the extent that this observation is remotely reasonable, it's only in the sense that you can code up one logic in another. Which, well, all the world's a TM, as they say... Anyways, I think the argument over whether type theory is a successful foundations for CS research and practice is already a closed issue. It demonstrably is. So is set theory.

by nmrm2 11y ago

ScottBurson 11y ago

I'm guessing LEM = Law of the Excluded Middle.

nmrm2 11y ago
Yes.

pron 11y ago

> 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. TLA+ has them, too. > in-so-far as one realizes that other people might have different experiences and so might (just as validly) consider other formalisms more familiar. So you think some people are more familiar with type theory than with undergrad-level set theory (ZF)? > sometimes, the type theoretic approach really is simpler, more familiar, and more flexible. E.g., in the case of this dissertation I don't see it (probably because my type theory is very, very basic; I'm an algorithm's guy and the thought that a data-structure of mine might need type theory to be specified makes me shudder), as in I fail to see anything that isn't readily expressible in simple classical logic + temporal logic. Could you explain?

nmrm2 11y ago
> TLA+ has them, too. Like I said, modus operandi matters. If I have to perform another model checking routine (possibly on an infinite state space) to slightly generalize a theorem, then in many cases that means I never really had a useful proof of it in the first place. Also, Coq's mathematics library is extensive and often closely follows the proofs found in graduate mathematics text books. Last I looked into TLA+, it was squarely focused on algorithms and hardware (not even CS-related mathematics more generally -- specifically algorithms and hardware). > So you think some people are more familiar with type theory than with undergrad-level set theory (ZF)? Do I think there exists some population of people who are "more familiar" with type theory than with ZF? Yes, starting, for example, with every researcher whose primary area of study is type theory. In fact, I think that anyone who doesn't honestly believe there are such people must have an extremely low opinion of quite a number of very smart people. (Also, set theory qua set theory gets really disgusting and kludgey really quickly, and is something that almost no undergraduate (or even phd student) is exposed to these days. The "set theory" you see in a discrete math course kind of barely scrapes definitions. I think most people who posit that "set theory" is nice and simple must've never really dove deem into the actual theory of set theory...) (Also, most real math these days quickly abstracts away from germanely set theoretic constructions. Mathematicians don't work in ZF. They do not. Most will tell you they do not, if they even know what ZF is. Which a lot won't, because their undergrad discrete math course is probably the last time they saw a truly formal derivation. And the mathematicians who do know what ZF is often can't regurgitate an axiomatization of ZF. If you tell a mathematician that all of math is just set theory, most will chuckle and wink and say "why, yes, yes it is", and hopefully you're in on the joke...) > I don't see it... I fail to see anything that isn't readily expressible in simple classical logic + temporal logic. Could you explain? Did you read this dissertation's explanation of why separation logic is important? To the extent that this observation is remotely reasonable, it's only in the sense that you can code up one logic in another. Which, well, all the world's a TM, as they say... Anyways, I think the argument over whether type theory is a successful foundations for CS research and practice is already a closed issue. It demonstrably is. So is set theory.