3 ms·

I guess "fighting" really is an appropriate word for what he's doing when he describes or-introduction as the "Act-Stupid"-rule in that composition paper. His

by joel_ms 10y ago

I guess "fighting" really is an appropriate word for what he's doing when he describes or-introduction as the "Act-Stupid"-rule in that composition paper. His alternative or-composition rule looks strange to me, since given either A or B it is entirely subsumed by simple implication, but his rule still seems to need both..? Or am I missing something about his notation? Section 6.3 also contains unsubstantiated claims about what is "popular among computer scientists" and what "many computer scientist" do or that they "denigrate the use of ordinary mathematics". I mean, this guy knows who he is talking about, why not call them out on the specifics? (He does reference one paper, and then attacks it by comparing it to a specification he worked on, which he does not reference.) He's obviously way smarter than me, and I think I understand his general position, but it's hard to get at his arguments when he wraps them in some much hostility. Personally I'm more interested and fascinated by the stuff going on in the Milner camp, so I'm obviously biased against him. But I do think the most fruitful approach is to have many people working in different directions and seeing what falls out, instead of trying to prove a priori that a research direction is useless.

pron 10y ago
> I guess "fighting" really is an appropriate word for what he's doing Oh, that article is especially trollish, but there are articles like that in both camps. > His alternative or-composition rule looks strange to me, since given either A or B it is entirely subsumed by simple implication, but his rule still seems to need both..? It's not about "needing" both, but about how proofs are decomposed. Sometimes you need to prove `A ∨ B ⇒ C`; that's your proof goal. To do that, you prove `A ⇒ C` and `B ⇒ C`. That's all. If you look at basic texts about formal reasoning, they're full of such rules (see, e.g. https://en.wikipedia.org/wiki/Natural_deduction https://en.wikipedia.org/wiki/Natural_deduction) But from a pragmatic perspective, I think this is clear: if you want to formally reason about large, real-world programs today (especially if they're concurrent or distributed) "Lamport's" approach is the only affordable way to do it. It is also mathematically simple, very elegant and fun. Whatever you're interested in academically, it also covers the most important concepts anyway (refinement/abstraction relations, inductive invariance), and, in the end how you work and think is basically the same.
- joel_ms 10y ago
  >Oh, that article is especially trollish, but there are articles like that in both camps Do you have any examples? >Sometimes you need to prove `A ∨ B ⇒ C`; that's your proof goal. To do that, you prove `A ⇒ C` and `B ⇒ C`. That's all. Yeah, I was just confused, it's just or-elimination with a different notation.
  - pron 10y ago
    > Do you have any examples? https://existentialtype.wordpress.com/2011/03/16/languages-and-machines/ https://existentialtype.wordpress.com/2011/03/16/languages-a... https://www.quora.com/What-is-Lambda-Calculus-in-laymans-terms/answer/Robert-Harper https://www.quora.com/What-is-Lambda-Calculus-in-laymans-ter... I wrote about some aspects of this mutual... hmm... let's call it skepticism here: https://pressron.wordpress.com/2016/08/30/what-we-talk-about-when-we-talk-about-computation/ https://pressron.wordpress.com/2016/08/30/what-we-talk-about...

by joel_ms 10y ago

pron 10y ago

> I guess "fighting" really is an appropriate word for what he's doing Oh, that article is especially trollish, but there are articles like that in both camps. > His alternative or-composition rule looks strange to me, since given either A or B it is entirely subsumed by simple implication, but his rule still seems to need both..? It's not about "needing" both, but about how proofs are decomposed. Sometimes you need to prove `A ∨ B ⇒ C`; that's your proof goal. To do that, you prove `A ⇒ C` and `B ⇒ C`. That's all. If you look at basic texts about formal reasoning, they're full of such rules (see, e.g. https://en.wikipedia.org/wiki/Natural_deduction https://en.wikipedia.org/wiki/Natural_deduction) But from a pragmatic perspective, I think this is clear: if you want to formally reason about large, real-world programs today (especially if they're concurrent or distributed) "Lamport's" approach is the only affordable way to do it. It is also mathematically simple, very elegant and fun. Whatever you're interested in academically, it also covers the most important concepts anyway (refinement/abstraction relations, inductive invariance), and, in the end how you work and think is basically the same.

joel_ms 10y ago
>Oh, that article is especially trollish, but there are articles like that in both camps Do you have any examples? >Sometimes you need to prove `A ∨ B ⇒ C`; that's your proof goal. To do that, you prove `A ⇒ C` and `B ⇒ C`. That's all. Yeah, I was just confused, it's just or-elimination with a different notation.
- pron 10y ago
  > Do you have any examples? https://existentialtype.wordpress.com/2011/03/16/languages-and-machines/ https://existentialtype.wordpress.com/2011/03/16/languages-a... https://www.quora.com/What-is-Lambda-Calculus-in-laymans-terms/answer/Robert-Harper https://www.quora.com/What-is-Lambda-Calculus-in-laymans-ter... I wrote about some aspects of this mutual... hmm... let's call it skepticism here: https://pressron.wordpress.com/2016/08/30/what-we-talk-about-when-we-talk-about-computation/ https://pressron.wordpress.com/2016/08/30/what-we-talk-about...