Re:Mathematical Reasoning and Distributed Systems by Erik Me...
by pron on Sunday December 04, 2016 @03:41PM
(#13101672)
> 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.
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.