Mathematical Reasoning and Distributed Systems by Erik Meijer and Leslie Lamport

They have, but much less so than people in the "temporal logic tradition". Type theory-based formal methods are virtually nonexistent in the industry (and the word virtually could probably be replaced with literally if we don't count joint industry-academia projects), while temporal logic is used to verify thousands of applications every year. The reason you see fewer papers is precisely because the approach is less mature. On the other hand, you find that papers using more traditional approaches are more cited (e.g., Lamport's first TLA paper alone has many more citations than any paper on type theory ever).

It is true, however, that PL theory is about much more than just formal methods (it is first and foremost about programming languages). The problem they're tackling is much harder and more ambitious, but so far they've had little success in the field.

  There is one case in which it’s worth doing the extra
  work: when the computer does a lot of it for you. 
  [..]
  In that case, the extra work introduced by decomposition 
  will be more than offset by the enormous benefit of using 
  model checking instead of human reasoning

I'm not from the Milner tradition, but I disagree with your criticisms of that tradition.

I think the key difference between TLA+ et al and the Milner tradition is automation.

In the Milner tradition, the automation follows sort of systematically from a proper formulation. So if you find the "right" way of formulating worst-case complexity, you get a lot more than just a way to state and hopefully prove some particular property -- you also get a way of automatically inferring that property and a sort of systematic way of baking your results into compiler infrastructure. This insight is perhaps masked by the fact that you can also formulate arbitrary properties in arbitrary styles in a dependent type theory... so to put it another way, the evidence for the fact that ML type systems are well-designed is the unification algorithm, not the type checker.

The TLA+ (et al.) story about automation is mostly "model checkers and invariant generators". In other words, the "hard stuff" is typically exogenous to the specification system/language. I know you might claim that model checking is sufficient, but I have a lot of experience with that approach and I respectfully disagree -- in part because the Milner tradition has produced a lot of insights that are often baked into model checkers and invariant generators. But also because this approach has fundamental scaling issues and designing around those constraints requires much more skill than advertised.

So while it's true that the type theory tradition is more difficult to understand, it's also true (IMO) that if you get something "right" in that tradition, it's far more powerful than getting something "right" in the TLA+ tradition.

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.

You're right that you can take a mathematical proof out of the realm of abstract math and it's new domain may not have all the guarantees we need, but this means we need to extend the system to account for the new domain (and within this domain, the proof is not valid).

But the poster doubled down on this idea that "there are constraints proofs ignore" within the existing domain. Outside of convenient proofs that upper division students provide, this is not true.

A good example of this process and the nature of "pure" CS interacting with the real world is the field of distributed databases. As the field has grown, proofs are expected to aggressively model real world conditions and in fact go further, modeling outright adversarial conditions unlikely to occur in the real world.

The point of mathetic's comment was to point out that a lot of ("computer science") mathematics goes into the design of the compilers and interpreters that software engineers use every day. And that it's rather ignorant for a user of one of these modern interpreters or compilers (even of a dynamically typed language!) to claim that this math doesn't matter or isn't useful.

> Remember the last couple of bug studies?

Which studies? There have been at least half a dozen high profile empirical studies about type systems in top tier conferences in the last 5 or 6 years, and probably dozens more in journals/conferences I don't follow.

The empirical evidence is predictably mixed. E.g. Hanenberg has published papers cutting in both directions re: usefulness of type systems.

Also, there's still very little empirical evidence about many type systems. There's a lot of Java vs. X comparison papers, but very few rigorous empirical studies on Haskell or SML or OCaml or Scala, for example. And I'm not aware of a single empirical comparative study on a dependently typed language.

> They didn't show type systems having an effect on reducing number of bugs

Actually, there are empirical studies that show type systems reduce bugs.

Also, as a separate matter, your summation of the available evidence is inaccurate to the point of absurdity. There is not a single shred of empirical evidence for your unconditional claim that type systems don't have an effect on reducing bugs. That hypothesis has never experimentally tested. Furthermore, the empirical data we have suggests that hypothesis is wrong.

Science works by looking at all the evidence and coming to informed conclusions. Cherry picking the N out of M studies that confirm your priors and then generalizing their results far beyond the parameters of the actual study is the opposite of scientific thought.

> but instead showed only significant correlation being number of LOCs.. And yet dynamically typed languages require fewer lines to express the same thing.

My OCaml programs are very often far shorter than my Python programs. Again, your unconditioned claims are getting you in trouble.

You probably mean to say something like "Java programs are usually longer than Python programs", in which case you have a reasonable critique of Java's type system, but not of type systems in general -- or even of the half dozen type systems that are radically different from Java's and in wide-spread use in production environments. And in fact, most adamant supports of type systems are probably some of the most ardent critics of Java's type system, so rejections of type systems on the basis of Java comparisons are a bit of a straw man IMO.

If there's a single thing that ALL of the various empirical PL design researchers could agree on, it's that the sort of unconditioned claims that are made in your post should be avoided.