3 ms·

> Formal methods will likely not help you - they can only show a _specification_ is sound, but not the _implementation_. I'm not sure where this idea came fro

> Formal methods will likely not help you - they can only show a _specification_ is sound, but not the _implementation_. I'm not sure where this idea came from. Are you in hardware? I guess in hardware that makes sense. Anyways, in software, formal methods can absolutely show that an implementation meets a specification. In fact, that has always been one of their canonical use cases in software systems, at least since the 70s or maybe early 80s. Formal methods can also be used with very ad hoc specifications, or with very general specifications, or increasingly without any explicitly specification at all (eg by inferring specifications). > cryptography suite from scratch or a large distributed system... Or aerospace software, or automotive software, or certain financial software, or industrial control systems, or any complex billing/access control, or... > there is zero advantage you would get over following best practices. I wrote a bunch of static analyses that checked for common configuration errors in Django apps which saved us many weekends. YMMV.

quixoticaxolotl 4y ago
I'm in software. > Anyways, in software, formal methods can absolutely show that an implementation meets a specification. In fact, that has always been one of their canonical use cases in software systems, at least since the 70s or maybe early 80s. To be clear, I'm talking about systems that go beyond simple property validation. Presumably, we're both talking about e.g. Ada SPARK, Alloy, TLA+, etc. I would hesitate to call a type system a formal method, for example, unless they use some notion of tactics like Idris, Coq and Lean do. Now there certainly exist formal methods that can show that a program meets a given specification and conforms to certain desirable properties. However, they cannot show that the program is bug-free, because many properties of a formally-verified system may be relaxed in real environments. When I say "sound", I mean the property of being bug-free. In OP's case, it would not help the OP reduce the frequency of bugs pushing to production - it would only give them confidence that they meet the spec, which is usually not what people writing internal tools are worried about. For industries where being safety-critical is not necessary, there is simply no meaningful advantage provided by formal methods over regression tests, clean refactoring and validators. While you can certainly use them, the benefits are slim. > Or aerospace software, or automotive software, or certain financial software, or industrial control systems, or any complex billing/access control, or... These are safety-critical industries, where things like temporal correctness, multiprocessor safety and other attributes matter - essentially, where you can model your system as process calculi and must demonstrate some invariants hold over the lifetime of the system given a specification. That is absolutely the domain of formal methods and where some formal verification is needed for certification. These industries are also the ones where you can ensure both certified hardware and software, so that formal verification actually does detect correctness bugs beyond what an integration test does. But OP has not said they are in any of these industries, and I don't think it's incumbent on me to be exhaustive in listing them when it's not core to OP's question. If OP's asking this question online instead of their colleagues, we can safely infer they're likely not in an industry that demands formal certification already.
- InefficientRed 4y ago
  > Presumably, we're both talking about e.g. Ada SPARK, Alloy, TLA+, etc. It's quite difficult to look at systems like Dafny or {J,C}BMC, in particular, and say "they can only show a _specification_ is sound, but not the _implementation_.", since those systems are definitely saying something about the implementation. Regarding "soundness", I think you're confused about terminology. I have no idea what it would mean for a spec to be bug-free; that seems equivalent to saying that a program is bug-free. Specs can have bugs for the same reason that implementations can have bugs. Anyways, "sound" has a well-understood meaning that is quite different from the one you're imposing. Soundness is a property of the entire system, not of individual formulas (specifications). A formal system/tool is sound if the system only admits proofs of a formula F whenever F is valid in the semantics. > But OP has not said they are in any of these industries, and I don't think it's incumbent on me to be exhaustive in listing them when it's not core to OP's question. You're missing the point, which are the ellipses. OP's question is "are formal methods worth it for me?" The appropriate answer has NOTHING to do with the type of code that OP is writing or their application domain. AWS components are not safety-critical in the sense of aircraft or automotive software, and they run on commodity hardware. Ditto for financial systems. But formal methods are applied successfully in both contexts. Again, I've used hand-rolled formal methods for Django apps as part of our deploy process and it's definitely saved us headaches. The implementation effort took very little time. A weekend and then a bit of ad hoc follow-up work. The rise of amazing parsers, really good implementation languages for this sort of code (scala, F#, ocaml), and fantastic SMT solvers (particularly string constraint solving) means that what used to require a "huge investment" can now be done in a weekend hackathon. Hardware is also making formal methods a cheaper prospect. Lately I've been playing with a small cluster of 64 core processors during off-hours and the amount of brute force search you can do in a weekend is pretty incredible. Formal Methods are often cheap and easy to implement, but they do have a high up-front human capital cost/learning curve. You need to know how to coalesce a class of bugs into a mathematical description. And then how to check that mathematical description against code by hacking together parsers, AST rewrites, and SMT solvers. The idea that this takes months or years of even weeks of time is pretty dated. A learned hand can get a lot done in a weekend.

quixoticaxolotl 4y ago

I'm in software. > Anyways, in software, formal methods can absolutely show that an implementation meets a specification. In fact, that has always been one of their canonical use cases in software systems, at least since the 70s or maybe early 80s. To be clear, I'm talking about systems that go beyond simple property validation. Presumably, we're both talking about e.g. Ada SPARK, Alloy, TLA+, etc. I would hesitate to call a type system a formal method, for example, unless they use some notion of tactics like Idris, Coq and Lean do. Now there certainly exist formal methods that can show that a program meets a given specification and conforms to certain desirable properties. However, they cannot show that the program is bug-free, because many properties of a formally-verified system may be relaxed in real environments. When I say "sound", I mean the property of being bug-free. In OP's case, it would not help the OP reduce the frequency of bugs pushing to production - it would only give them confidence that they meet the spec, which is usually not what people writing internal tools are worried about. For industries where being safety-critical is not necessary, there is simply no meaningful advantage provided by formal methods over regression tests, clean refactoring and validators. While you can certainly use them, the benefits are slim. > Or aerospace software, or automotive software, or certain financial software, or industrial control systems, or any complex billing/access control, or... These are safety-critical industries, where things like temporal correctness, multiprocessor safety and other attributes matter - essentially, where you can model your system as process calculi and must demonstrate some invariants hold over the lifetime of the system given a specification. That is absolutely the domain of formal methods and where some formal verification is needed for certification. These industries are also the ones where you can ensure both certified hardware and software, so that formal verification actually does detect correctness bugs beyond what an integration test does. But OP has not said they are in any of these industries, and I don't think it's incumbent on me to be exhaustive in listing them when it's not core to OP's question. If OP's asking this question online instead of their colleagues, we can safely infer they're likely not in an industry that demands formal certification already.

InefficientRed 4y ago
> Presumably, we're both talking about e.g. Ada SPARK, Alloy, TLA+, etc. It's quite difficult to look at systems like Dafny or {J,C}BMC, in particular, and say "they can only show a _specification_ is sound, but not the _implementation_.", since those systems are definitely saying something about the implementation. Regarding "soundness", I think you're confused about terminology. I have no idea what it would mean for a spec to be bug-free; that seems equivalent to saying that a program is bug-free. Specs can have bugs for the same reason that implementations can have bugs. Anyways, "sound" has a well-understood meaning that is quite different from the one you're imposing. Soundness is a property of the entire system, not of individual formulas (specifications). A formal system/tool is sound if the system only admits proofs of a formula F whenever F is valid in the semantics. > But OP has not said they are in any of these industries, and I don't think it's incumbent on me to be exhaustive in listing them when it's not core to OP's question. You're missing the point, which are the ellipses. OP's question is "are formal methods worth it for me?" The appropriate answer has NOTHING to do with the type of code that OP is writing or their application domain. AWS components are not safety-critical in the sense of aircraft or automotive software, and they run on commodity hardware. Ditto for financial systems. But formal methods are applied successfully in both contexts. Again, I've used hand-rolled formal methods for Django apps as part of our deploy process and it's definitely saved us headaches. The implementation effort took very little time. A weekend and then a bit of ad hoc follow-up work. The rise of amazing parsers, really good implementation languages for this sort of code (scala, F#, ocaml), and fantastic SMT solvers (particularly string constraint solving) means that what used to require a "huge investment" can now be done in a weekend hackathon. Hardware is also making formal methods a cheaper prospect. Lately I've been playing with a small cluster of 64 core processors during off-hours and the amount of brute force search you can do in a weekend is pretty incredible. Formal Methods are often cheap and easy to implement, but they do have a high up-front human capital cost/learning curve. You need to know how to coalesce a class of bugs into a mathematical description. And then how to check that mathematical description against code by hacking together parsers, AST rewrites, and SMT solvers. The idea that this takes months or years of even weeks of time is pretty dated. A learned hand can get a lot done in a weekend.