7 ms·

I am currently hearing "formal Systems" at my university and that got me interested a bit. Can somebody comment why in practice it's so hard? In and ideal world

I am currently hearing "formal Systems" at my university and that got me interested a bit. Can somebody comment why in practice it's so hard? In and ideal world I would image that certain languages are easier to prove (haskell vs C) and with the right tooling it should be able to prove many things quickly. Some things will always remain hard, but right now i don't see formal proofs of programs at all (i only hear some rumours that some companies use it at some small scale). So what's holding it back from being practical? Not enough engineer Man-power? Or is our theoretical understanding still not developed enough?

tom_mellior 10y ago
> In and ideal world I would image that certain languages are easier to prove (haskell vs C) It is. That's why Coq is a pure functional language, rather more like Haskell than like C. > and with the right tooling it should be able to prove many things quickly Yes, this should be possible, and it is possible. If you mean you want it to be automated: Isabelle/HOL has more automation than Coq. For many simple things, it suffices to tell Isabelle, essentially, to perform induction on a given variable and from that to try to find a proof automatically. It builds on several external provers to implement this. What is difficult is for the system to know which existing lemmas to reuse and how to combine them. It's a bit like your math homework, except that these systems know more lemmas (i.e., have a larger search space) and are not always good at ranking them by relevance. > right now i don't see formal proofs of programs at all (i only hear some rumours that some companies use it at some small scale) Look up SEL4 and CompCert for a start.
- LeanderK 10y ago
  OK, so if i want to build a program that proves my haskell code with a similar ease as using quickcheck[0] it would be possible, its just that nobody has done it yet and not that i would be nearly useless because i wouldn't be able to prove the most basic every-day functions. I would guess an database of previously proved lemmas for all the used libraries would help, so that you don't have to recompute everything. [0] quickcheck is an awesome library that generates unit-tests for specified properties (like: "for all lists s: length(sort(s)) = length(s)", i would then just generate a few hundred lists and check whether the property got violated)
  - tom_mellior 10y ago
    > OK, so if i want to build a program that proves my haskell code with a similar ease as using quickcheck[0] it would be possible, its just that nobody has done it yet Yes, kind of. For certain values of "similar ease" and "Haskell". AFAIK Agda is pretty much Haskell, but its proving part is not all that automatic. On the other hand, Isabelle has a lot of proof automation (and includes an implementation of QuickCheck that it applies automatically to every property you state when you start proving it!), but its own variant of functional programming is not exactly Haskell. I think you can extract Haskell programs from it, though. > I would guess an database of previously proved lemmas for all the used libraries would help It may help, but it may also confuse the proof search if it gets lost in a sea of irrelevant lemmas. Which is what I was trying to say above, I never said anything about recomputing stuff.
  - bbcbasic 10y ago
    Liquid Haskell is worth a look
    - LeanderK 10y ago
      i was not aware of what's going on with Liquid Haskell! This dissertation[0] just came out and looks like to be exactly what i had in mind! [0] http://goto.ucsd.edu/~nvazou/thesis/main.pdf http://goto.ucsd.edu/~nvazou/thesis/main.pdf
- pron 10y ago
  >> and with the right tooling it should be able to prove many things quickly > Yes, this should be possible, and it is possible. Regardless of the formal tool you use, be it Coq, Idris, TLA+ or Isabelle, proving what you need proving most -- the non-trivial stuff -- is never quick and easy. The reason it's hard to prove non-trivial algorithms correct is because it's hard to write non-trivial algorithms correctly. Temporal logic, HOL, SMT, dependent types, model checking, abstract interpretation -- they're all useful tools, but in the end, to make the utmost of formal methods, and understand the difficulties and possibilities, one must first understand the nature of algorithms and how they work, and this is always the same, regardless of the particular formalism used. Personally, I've found TLA+ to best isolate the core of the issue with as few distractions as possible, and others may find other formalisms to better suit how they think, but the essential problem is always the same. It is true, however, that some formal tools impose more accidental complexity than others. The ones that are most refined are those that are used by real engineers on large real-world software every day, like SCADE, TLA+, SPARK etc., while things like Coq and Agda are mostly aimed at researchers and designed to let them explore new ideas. In practice, the industry uses automated formal methods -- SMT solvers and model checkers -- almost exclusively, with interactive deductive proof used to tie results together or to fill in a few missing gaps. Interactive theorem proving is currently too costly as a primary tool for use in real-world software, in all but the most high-assurance settings. > Look up SEL4 and CompCert for a start. seL4 and CompCert -- while great achievements -- are neither good examples of formal methods, nor are they particularly encouraging. For one, they were academic projects that took world experts years of effort for what amounts to very small software as far as industry software goes (comparable to a ~10KLOC C program). For another, the kind of verification they required is what's known as "end-to-end", namely global correctness properties are proven all the way down to machine code. This level of correctness is unnecessary for 99.99% of software; perhaps even for no software at all. Much better examples of the use of formal methods in industry include the use of SCADE to write thousands of safety-critical, hard realtime software every year; the use of Z and Ada SPARK by AltranUK to write large, complex defense software; the use of SPIN and other model checkers to find flaws in hardware designs, the use of B-Method in the railway sector, and the use of TLA+ at Amazon, Oracle and other companies for complex server-side services.
  - 10y ago
- mrefj 10y ago
  > If you mean you want it to be automated ACL2 is an alternative that strives to strike a balance between interaction and automation. - It is more automated than any of the interactive theorem provers including Isabelle/HOL, Coq, etc. - Its authors received the ACM software system award in 2005. -It is used in commercial products since several years in companies including AMD, Centaur , Rockwell Collins, etc. There is a not-so comprehensive but yet impressive list of applications here: http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html http://www.cs.utexas.edu/users/moore/publications/acl2-paper... - Also, since the language is a subset of Common-lisp, any one who knows a bit of programming can very quickly start using ACL2. One does not need to learn type theory/logical formalism to start using it. It has an eclipse plugin that is used by first and second year undergraduate students (http://acl2s.ccs.neu.edu/acl2s/doc/ http://acl2s.ccs.neu.edu/acl2s/doc/).
pron 10y ago
In addition to the discussion in the sister comments about specific details of formal methods, there are certainly theoretical difficulties. See this post that I wrote some months ago: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c... Also, formal methods, like AI, suffered a "research winter" after making grand promises that they weren't actually able to keep. The hype initially drew a lot of funding, and with the disappointment came a period of relative neglect. Have those two unsubstantiated-hype-prone disciplines learned the lessons and are able to lower their sights to what's attainable, or will they end up wasting a lot of time and money? I guess we'll see. I think that at least the formal methods community is more cautious now, and focuses on reducing various classes of bugs rather than promising affordable 100% correct software.

tom_mellior 10y ago

> In and ideal world I would image that certain languages are easier to prove (haskell vs C) It is. That's why Coq is a pure functional language, rather more like Haskell than like C. > and with the right tooling it should be able to prove many things quickly Yes, this should be possible, and it is possible. If you mean you want it to be automated: Isabelle/HOL has more automation than Coq. For many simple things, it suffices to tell Isabelle, essentially, to perform induction on a given variable and from that to try to find a proof automatically. It builds on several external provers to implement this. What is difficult is for the system to know which existing lemmas to reuse and how to combine them. It's a bit like your math homework, except that these systems know more lemmas (i.e., have a larger search space) and are not always good at ranking them by relevance. > right now i don't see formal proofs of programs at all (i only hear some rumours that some companies use it at some small scale) Look up SEL4 and CompCert for a start.

LeanderK 10y ago
OK, so if i want to build a program that proves my haskell code with a similar ease as using quickcheck[0] it would be possible, its just that nobody has done it yet and not that i would be nearly useless because i wouldn't be able to prove the most basic every-day functions. I would guess an database of previously proved lemmas for all the used libraries would help, so that you don't have to recompute everything. [0] quickcheck is an awesome library that generates unit-tests for specified properties (like: "for all lists s: length(sort(s)) = length(s)", i would then just generate a few hundred lists and check whether the property got violated)
- tom_mellior 10y ago
  > OK, so if i want to build a program that proves my haskell code with a similar ease as using quickcheck[0] it would be possible, its just that nobody has done it yet Yes, kind of. For certain values of "similar ease" and "Haskell". AFAIK Agda is pretty much Haskell, but its proving part is not all that automatic. On the other hand, Isabelle has a lot of proof automation (and includes an implementation of QuickCheck that it applies automatically to every property you state when you start proving it!), but its own variant of functional programming is not exactly Haskell. I think you can extract Haskell programs from it, though. > I would guess an database of previously proved lemmas for all the used libraries would help It may help, but it may also confuse the proof search if it gets lost in a sea of irrelevant lemmas. Which is what I was trying to say above, I never said anything about recomputing stuff.
- bbcbasic 10y ago
  Liquid Haskell is worth a look
  - LeanderK 10y ago
    i was not aware of what's going on with Liquid Haskell! This dissertation[0] just came out and looks like to be exactly what i had in mind! [0] http://goto.ucsd.edu/~nvazou/thesis/main.pdf http://goto.ucsd.edu/~nvazou/thesis/main.pdf
pron 10y ago
>> and with the right tooling it should be able to prove many things quickly > Yes, this should be possible, and it is possible. Regardless of the formal tool you use, be it Coq, Idris, TLA+ or Isabelle, proving what you need proving most -- the non-trivial stuff -- is never quick and easy. The reason it's hard to prove non-trivial algorithms correct is because it's hard to write non-trivial algorithms correctly. Temporal logic, HOL, SMT, dependent types, model checking, abstract interpretation -- they're all useful tools, but in the end, to make the utmost of formal methods, and understand the difficulties and possibilities, one must first understand the nature of algorithms and how they work, and this is always the same, regardless of the particular formalism used. Personally, I've found TLA+ to best isolate the core of the issue with as few distractions as possible, and others may find other formalisms to better suit how they think, but the essential problem is always the same. It is true, however, that some formal tools impose more accidental complexity than others. The ones that are most refined are those that are used by real engineers on large real-world software every day, like SCADE, TLA+, SPARK etc., while things like Coq and Agda are mostly aimed at researchers and designed to let them explore new ideas. In practice, the industry uses automated formal methods -- SMT solvers and model checkers -- almost exclusively, with interactive deductive proof used to tie results together or to fill in a few missing gaps. Interactive theorem proving is currently too costly as a primary tool for use in real-world software, in all but the most high-assurance settings. > Look up SEL4 and CompCert for a start. seL4 and CompCert -- while great achievements -- are neither good examples of formal methods, nor are they particularly encouraging. For one, they were academic projects that took world experts years of effort for what amounts to very small software as far as industry software goes (comparable to a ~10KLOC C program). For another, the kind of verification they required is what's known as "end-to-end", namely global correctness properties are proven all the way down to machine code. This level of correctness is unnecessary for 99.99% of software; perhaps even for no software at all. Much better examples of the use of formal methods in industry include the use of SCADE to write thousands of safety-critical, hard realtime software every year; the use of Z and Ada SPARK by AltranUK to write large, complex defense software; the use of SPIN and other model checkers to find flaws in hardware designs, the use of B-Method in the railway sector, and the use of TLA+ at Amazon, Oracle and other companies for complex server-side services.
- 10y ago
mrefj 10y ago
> If you mean you want it to be automated ACL2 is an alternative that strives to strike a balance between interaction and automation. - It is more automated than any of the interactive theorem provers including Isabelle/HOL, Coq, etc. - Its authors received the ACM software system award in 2005. -It is used in commercial products since several years in companies including AMD, Centaur , Rockwell Collins, etc. There is a not-so comprehensive but yet impressive list of applications here: http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html http://www.cs.utexas.edu/users/moore/publications/acl2-paper... - Also, since the language is a subset of Common-lisp, any one who knows a bit of programming can very quickly start using ACL2. One does not need to learn type theory/logical formalism to start using it. It has an eclipse plugin that is used by first and second year undergraduate students (http://acl2s.ccs.neu.edu/acl2s/doc/ http://acl2s.ccs.neu.edu/acl2s/doc/).

pron 10y ago

In addition to the discussion in the sister comments about specific details of formal methods, there are certainly theoretical difficulties. See this post that I wrote some months ago: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c... Also, formal methods, like AI, suffered a "research winter" after making grand promises that they weren't actually able to keep. The hype initially drew a lot of funding, and with the disappointment came a period of relative neglect. Have those two unsubstantiated-hype-prone disciplines learned the lessons and are able to lower their sights to what's attainable, or will they end up wasting a lot of time and money? I guess we'll see. I think that at least the formal methods community is more cautious now, and focuses on reducing various classes of bugs rather than promising affordable 100% correct software.