3 ms·

> Type theory-based formal methods are virtually nonexistent in the industry I mean, all of the ML-derivative languages are in very wide-spread use. I guess yo

> Type theory-based formal methods are virtually nonexistent in the industry 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).

pron 10y ago
> 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. 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.

pron 10y ago

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