I mean, all of the ML-derivative languages are in very wide-spread use. I guess you could argue that type systems aren't formal methods, but I'd disagree -- especially in the case of systems with effective type inference, which is essentially a bit of theorem proving baked into your language.
I would guess that Algorithm W (and derivatives) are the most successful and most widely used formal methods tool in the world today.
> ...if we don't count joint industry-academia projects
The same is true for most formal methods (FWIW I consider MSR and similar labs squarely in the "academia" side of that divide...) It's not even clear to me that this is a bad thing, actually. Maybe for highly critical systems it makes sense for companies to contract with boutique formal methods firms.
More generally, what I meant by "incredibly productive" is that a lot of the ideas in their work are equally applicable to other systems that aren't in that tradition. So that even if you aren't working the Milner tradition (which I man not), you may still find this work worth knowing about and borrowing from (which I do).
The kind of properties those type systems that are in relatively widespread use prove are not even remotely close to those you'd call "program correctness".
> I would guess that Algorithm W (and derivatives) are the most successful and most widely used formal methods tool in the world today.
OK, but that's an extremely weak formal method; weaker than some static analysis tools, that are also in widespread use.
> The same is true for most formal methods
Not really. SCADE is quite popular in safety-critical hard realtime systems, and TLA+, while far from "popular" is being regularly used at Amazon, Oracle and smaller companies without any assistance from academia. Other tools, like Z and Ada SPARK (both used by Altran), B-Method (popular in railway software) or SPIN are also regularly used in the industry.
> you may still find this work worth knowing about and borrowing from (which I do).
Sure, but it goes both ways. I've seen a paper about proving the correctness of some control systems for quadcopters in Coq, and they basically used Lamport's TLA in Coq.
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.