4 ms·

I read a lot of good ones but I'll answer what was most important rather than best. We're seeing a revival of formal methods ranging from lightweight (TLA+) to

I read a lot of good ones but I'll answer what was most important rather than best. We're seeing a revival of formal methods ranging from lightweight (TLA+) to heavy. Two problems are in my sight: lack of framework plus consistent, empirical data for evaluating how suitable a given method is for a specific project or company; many who would use lightweight or practical methods will quit because someone convinced them to start with heavy ones. The paper below is a start on the former: https://www.scch.at/de/rse-news/passende-formale-methon?file=files/Dokumente/SCCH_Web/Downloads/Downloads_2015/DownloadBilder/Neu_SCCH-TR-1603_FormalMethodsComparison.pdf https://www.scch.at/de/rse-news/passende-formale-methon?file... I think that was a great start on an evalution criteria because its comparisons match what I read in the various experience reports. ASM's and TLA+ coming in the lead on usability but B method on code generation. It will also help to note what projects have been completed or reusable libraries available in each. A person building verified compilers for functional languages might want to learn Isabelle/HOL due to CakeML, doing a new TLS extension learn F* due to miTLS, type-safe assembly learn Coq due to CoqASM, and so on. For the other issue, I made a proposal on HN first and then on Lobste.rs about avoiding people quitting early from finding formal methods too overwhelming or useless. I proposed having a default intro or lure that matched the goals of different people to tools with a warning of some's difficulty. It got some interesting responses (below) I'll turn into a mini-essay with links eventually. https://lobste.rs/s/n7v658/your_thoughts_on_this_advice_those https://lobste.rs/s/n7v658/your_thoughts_on_this_advice_thos...

pron 9y ago
TLA+ is by no means considered a lightweight formal method. It is proven relatively complete, i.e. anything that can be proven about a program, can be proven in TLA+. It can be used to only partially specify and verify a system, but so can Coq (usually, the term lightweight formal methods is applied to tools that can only specify/verify partially, or that that is their main intent). The main difference between TLA+ and other "deep" formal tools (Coq/Isabelle/Lean etc.) is that it is much easier to learn and apply. This is not because it is by any means lighter-weight in terms of software verification, but because of specific design choice which make it unsuitable to the primary goal of those other tools, namely formal proofs of "high" mathematics and the definition and exploration of novel logics. Those tools are so much harder to learn and use than TLA+ mainly because verifying programs is not their main goal. As a general math/logic proof assistant, TLA+ could certainly be considered lightweight, though :)
- nickpsecurity 9y ago
  Maybe I should've said TLA+ w/ model checking since that's definitely lightweight versus full, formal verification. Far as Lean, it's specifically designed for proving stuff about "complex systems."
  - pron 9y ago
    > Maybe I should've said TLA+ w/ model checking since that's definitely lightweight versus full, formal verification. Why do you say that? Model checking is the most common form of full formal verification. It is true that because most TLA+ specifications -- unlike most software that's verified with model checkers -- has an infinite state space and that TLC, the model checker that's packaged with the TLA+ toolbox is an explicit state exploration model-checker with not support for infinite state spaces, then most of the time it is used on a finite-state derived specification and so doesn't fully verify the spec. But that is, AFAIK, not what is normally meant by "lightweight formal methods" (although I am not sure there is a very precise, well-accepted definition). But people take all sorts of short-cuts when working in Coq, too, and very rarely fully verify every aspect of the program. In fact, the only programs that were ever "fully" verified was 1. very small (much smaller than the vast majority of programs used in industry; I think jQuery is several times bigger than the biggest program ever "fully" verified end-to-end), 2. were heavily simplified in terms of algorithms used, and 3. took a loong time and required experts. So if that's how you'd classify "lightweight", then "full" doesn't exist in any meaningful sense. > Far as Lean, it's specifically designed for proving stuff about "complex systems." No, it's a Coq-style, general-purpose proof assistant. In any event, Coq, Lean and Isabelle are all designed for researchers. They are not aimed at industrial use at all. I know that the people behind Lean -- all accomplished experts in formal mathematics -- have made some claims about its suitability for verifying software, but AFAIK, none of them has any practical experience in software verification in industry, and so I find their claims to be entirely hypothetical. It's a beautiful proof assistant, but pragmatic software verification is not its first nor second goal. In contrast, TLA+ was designed with the help of actual "ordinary" industry engineers (at Compaq), who were using it for a large, real-world project, as it was being developed. That's the main difference between TLA+ and Coq/Lean -- it was designed as a product for engineers, not as a research tool for logicians.

pron 9y ago

TLA+ is by no means considered a lightweight formal method. It is proven relatively complete, i.e. anything that can be proven about a program, can be proven in TLA+. It can be used to only partially specify and verify a system, but so can Coq (usually, the term lightweight formal methods is applied to tools that can only specify/verify partially, or that that is their main intent). The main difference between TLA+ and other "deep" formal tools (Coq/Isabelle/Lean etc.) is that it is much easier to learn and apply. This is not because it is by any means lighter-weight in terms of software verification, but because of specific design choice which make it unsuitable to the primary goal of those other tools, namely formal proofs of "high" mathematics and the definition and exploration of novel logics. Those tools are so much harder to learn and use than TLA+ mainly because verifying programs is not their main goal. As a general math/logic proof assistant, TLA+ could certainly be considered lightweight, though :)

nickpsecurity 9y ago
Maybe I should've said TLA+ w/ model checking since that's definitely lightweight versus full, formal verification. Far as Lean, it's specifically designed for proving stuff about "complex systems."
- pron 9y ago
  > Maybe I should've said TLA+ w/ model checking since that's definitely lightweight versus full, formal verification. Why do you say that? Model checking is the most common form of full formal verification. It is true that because most TLA+ specifications -- unlike most software that's verified with model checkers -- has an infinite state space and that TLC, the model checker that's packaged with the TLA+ toolbox is an explicit state exploration model-checker with not support for infinite state spaces, then most of the time it is used on a finite-state derived specification and so doesn't fully verify the spec. But that is, AFAIK, not what is normally meant by "lightweight formal methods" (although I am not sure there is a very precise, well-accepted definition). But people take all sorts of short-cuts when working in Coq, too, and very rarely fully verify every aspect of the program. In fact, the only programs that were ever "fully" verified was 1. very small (much smaller than the vast majority of programs used in industry; I think jQuery is several times bigger than the biggest program ever "fully" verified end-to-end), 2. were heavily simplified in terms of algorithms used, and 3. took a loong time and required experts. So if that's how you'd classify "lightweight", then "full" doesn't exist in any meaningful sense. > Far as Lean, it's specifically designed for proving stuff about "complex systems." No, it's a Coq-style, general-purpose proof assistant. In any event, Coq, Lean and Isabelle are all designed for researchers. They are not aimed at industrial use at all. I know that the people behind Lean -- all accomplished experts in formal mathematics -- have made some claims about its suitability for verifying software, but AFAIK, none of them has any practical experience in software verification in industry, and so I find their claims to be entirely hypothetical. It's a beautiful proof assistant, but pragmatic software verification is not its first nor second goal. In contrast, TLA+ was designed with the help of actual "ordinary" industry engineers (at Compaq), who were using it for a large, real-world project, as it was being developed. That's the main difference between TLA+ and Coq/Lean -- it was designed as a product for engineers, not as a research tool for logicians.