5 ms·

> 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 slightl

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

pron 11y ago
> If I have to perform another model checking routine Why model checking? TLA+ is not a model checker. It's a specification and proof language. There is a model checker that can check TLA+ specs, just as there is a proof assistant that can check TLA+ proofs. > must have an extremely low opinion of quite a number of very smart people. Why low opinion? Type theory isn't "smarter", it's just more obscure. > 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... Thankfully, that basic set theory -- the one that barely scrapes the definition -- is all that's required to specify real-world programs. > Did you read this dissertation's explanation of why separation logic is important? Skimmed it. Unless I'm missing something (which is quite possible) it seems very straightforward to use in TLA+: you just define the operators just as they're defined in the paper. There's no need to "code" the logic in any arcane or non-obvious way; just define it. In fact, this short paper describes doing just that and it seems pretty basic: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.570.3798&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.570... > 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. It never even crossed my mind to make the case that it isn't. That type theory is an interesting topic for research is obvious. I also never implied that dependent-type tools can't do the job; as you say, they demonstrably can. I simply asked if I -- a programmer working in the industry -- had a program I wished to verify, whether there was a reason why I would reach for a dependent-type tool vs. a classical logic tool. So far, I don't see why I should. It seems to basically boil down (at least according to the responses in this thread) to whether I prefer working with direct, classical logic or with dependent types.
- nmrm2 11y ago
  > TLA+ is not a model checker. It's a specification and proof language. There is a model checker that can check TLA+ specs, just as there is a proof assistant that can check TLA+ proofs. For the third (!) time, modus operandi matters. Coq's huge library of tactics and proofs of facts that TLA+ might just throw at a model checker are, in my experience, very useful starting points for things that can't be model checked. Ostentibly TLA+ could build up an equivalent library of tactics and proofs. > Why low opinion? Even supposing type theory is "more obscure", it's pretty hard to believe that someone could study it for 30 years and not understand it better (in some sense) than ZF. That's a pretty extraordinary claim. > basic set theory -- the one that barely scrapes the definition -- is all that's required to specify real-world programs. Not really -- you often need non-trivial constructions when proving properties about rewrite systems within set theory. Those constructions are much harder to understand than induction on algebraic datatypes, which is why type theoretic approaches have dominated in formalization of programming languages. >Unless I'm missing something... I'm disinclined the dismiss separation logic just because you can code up some of its ideas in another logic (in a way that counts as a novel contribution worthy of publication, no less). The clarity with which separation logic presents the idea and use of the separating conjunction has obviously influenced the paper you cited. I would think this is reason enough to summarily dismiss these "everything's a TM"-style arguments you're making here. The authors of the paper you cited are only not using separation logic in a kind of meaningless sense IMO. > So far, I don't see why I should. This sentiment kind of reminds me of people who have never typeset mathematics complaining that LaTeX is useless... which is to say, perhaps you simply aren't interested in and so don't care about the use cases where Coq shines? Lots of people -- including me -- have already pointed out a lot of these use-cases in this comment section. But really, based on the arc of this conversation, I would be enormously surprised if you chose to use Coq to prove X, even if there were a proveX tactic already written in Coq and the TLA+ implementation would take all day ;-)

by nmrm2 11y ago

pron 11y ago

> If I have to perform another model checking routine Why model checking? TLA+ is not a model checker. It's a specification and proof language. There is a model checker that can check TLA+ specs, just as there is a proof assistant that can check TLA+ proofs. > must have an extremely low opinion of quite a number of very smart people. Why low opinion? Type theory isn't "smarter", it's just more obscure. > 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... Thankfully, that basic set theory -- the one that barely scrapes the definition -- is all that's required to specify real-world programs. > Did you read this dissertation's explanation of why separation logic is important? Skimmed it. Unless I'm missing something (which is quite possible) it seems very straightforward to use in TLA+: you just define the operators just as they're defined in the paper. There's no need to "code" the logic in any arcane or non-obvious way; just define it. In fact, this short paper describes doing just that and it seems pretty basic: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.570.3798&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.570... > 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. It never even crossed my mind to make the case that it isn't. That type theory is an interesting topic for research is obvious. I also never implied that dependent-type tools can't do the job; as you say, they demonstrably can. I simply asked if I -- a programmer working in the industry -- had a program I wished to verify, whether there was a reason why I would reach for a dependent-type tool vs. a classical logic tool. So far, I don't see why I should. It seems to basically boil down (at least according to the responses in this thread) to whether I prefer working with direct, classical logic or with dependent types.

nmrm2 11y ago
> TLA+ is not a model checker. It's a specification and proof language. There is a model checker that can check TLA+ specs, just as there is a proof assistant that can check TLA+ proofs. For the third (!) time, modus operandi matters. Coq's huge library of tactics and proofs of facts that TLA+ might just throw at a model checker are, in my experience, very useful starting points for things that can't be model checked. Ostentibly TLA+ could build up an equivalent library of tactics and proofs. > Why low opinion? Even supposing type theory is "more obscure", it's pretty hard to believe that someone could study it for 30 years and not understand it better (in some sense) than ZF. That's a pretty extraordinary claim. > basic set theory -- the one that barely scrapes the definition -- is all that's required to specify real-world programs. Not really -- you often need non-trivial constructions when proving properties about rewrite systems within set theory. Those constructions are much harder to understand than induction on algebraic datatypes, which is why type theoretic approaches have dominated in formalization of programming languages. >Unless I'm missing something... I'm disinclined the dismiss separation logic just because you can code up some of its ideas in another logic (in a way that counts as a novel contribution worthy of publication, no less). The clarity with which separation logic presents the idea and use of the separating conjunction has obviously influenced the paper you cited. I would think this is reason enough to summarily dismiss these "everything's a TM"-style arguments you're making here. The authors of the paper you cited are only not using separation logic in a kind of meaningless sense IMO. > So far, I don't see why I should. This sentiment kind of reminds me of people who have never typeset mathematics complaining that LaTeX is useless... which is to say, perhaps you simply aren't interested in and so don't care about the use cases where Coq shines? Lots of people -- including me -- have already pointed out a lot of these use-cases in this comment section. But really, based on the arc of this conversation, I would be enormously surprised if you chose to use Coq to prove X, even if there were a proveX tactic already written in Coq and the TLA+ implementation would take all day ;-)