4 ms·

One major school of thought in formal methods is the type theory tradition. The one-sentence formal methods interpretation of this program is that types are the

One major school of thought in formal methods is the type theory tradition. The one-sentence formal methods interpretation of this program is that types are theorems and programs are proofs. The idea, basically, is to choose a type system that is expressive enough to encode interesting properties. Then, if your program has that type, you know that your program is correct with respect to the specification that is encoded in the type. It turns out that there are type theories in which arbitrary mathematical properties can be encoded and proven, so this approach is very versatile. Systems such as Coq, NuPRL, Idris, and Lean are in this tradition.+ Obviously, there are also other approaches to formal methods that are not built upon type theory. However, my experience is that the type theorists have been incredibly productive, so if you spend enough time doing formal methods you'll probably find some work done in the type theory tradition that's useful or relevant to any particular approach. + I'm not a type theorist and have reason to believe that certain type theorists would perhaps disagree with this characterization for reason that would be rather difficult for a non-type-theorist to understand, but hopefully this gives you a rough idea. Also, it's worth noting that those in the Milner tradition see their agenda as being far more than just one approach toward formal methods, and also as not being principally about types. But thinking about that tradition in terms of Coq et al. and props-as-types is the best way to understand its place in Formal Methods.

pron 10y ago
> However, my experience is that the type theorists have been incredibly productive 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.
- throwaway729 10y ago
  > 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

> However, my experience is that the type theorists have been incredibly productive 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.

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