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