4 ms·

This just FUD. Formal proofs are quite prevalent. Look at ACL2 for a start.

seanmcdirmid 11y ago
Not FUD at all. Pointing at a system doesn't provide any evidence that proofs are prevalent in industry. Check out: https://chess.eecs.berkeley.edu/hcssas/papers/Cleaveland-position-paper.pdf https://chess.eecs.berkeley.edu/hcssas/papers/Cleaveland-pos... > Although formal proofs of correctness are (rightly) touted as providing superior guarantees to those of testing, DO-178B makes no mention of formal methods, except in an Annex given over to techniques deemed not yet mature enough for certification purposes. Or http://ti.arc.nasa.gov/m/pub-archive/1023h/1023%20(Denney).pdf http://ti.arc.nasa.gov/m/pub-archive/1023h/1023%20(Denney).p...: > In principle, formal methods offer many advantages for aerospace software development: they can help to achieve ultra-high reliability, and they can be used to provide evidence of the reliability claims which can then be subjected to external scrutiny. However, despite years of research and many advances in the underlying formalisms of specification, semantics, and logic, formal methods are not much used in practice. In our opinion this is related to three major shortcomings. First, the application of formal methods is still expensive because they are labor- and knowledge-intensive. Second, they are difficult to scale up to complex systems because they are based on deep mathematical insights about the behavior of the systems (i.e., they rely on the “heroic proof”). Third, the proofs can be difficult to interpret, and typically stand in isolation from the original code. The situation will just get worse as we increasingly move away from hand written logic to machine learned logic. Now, there is probably a place for formal methods in this newer order, but it will take awhile for researchers to find it, and it is definitely not going to be at the level of verifying hand-encoded logic that doesn't exist.
- cscurmudgeon 11y ago
  I meant to point out formal verification is used in the industry quite a bit (not in aviation alone). 1. Replacing testing with formal verification at Intel (2009) http://link.springer.com/chapter/10.1007/978-3-642-02658-4_32 http://link.springer.com/chapter/10.1007/978-3-642-02658-4_3... 2. Fifteen years of formal property verification at Intel (2008) http://link.springer.com/chapter/10.1007/978-3-540-69850-0_8 http://link.springer.com/chapter/10.1007/978-3-540-69850-0_8 3. seL4: formal verification of an OS kernel http://dl.acm.org/citation.cfm?id=1629596 http://dl.acm.org/citation.cfm?id=1629596 There is such a big need that DARPA has even come up with a contest. http://www.darpa.mil/program/crowd-sourced-formal-verification http://www.darpa.mil/program/crowd-sourced-formal-verificati... I could go on, but I would rather not spend my time combating FUD and the general incivility here.
  - seanmcdirmid 11y ago
    Formal verification is used a lot, but it is not a rule and definitely not a requirement by the FAA for aircraft certification. The idea that formal verification would be obviously necessary for the logic of a self-driving car is what was being challenged here. You could call that FUD, but you obviously have an agenda to push, I guess.
    - cscurmudgeon 11y ago
      > not a requirement by the FAA for aircraft certification. I never said that. Where did you get that? > Safety critical systems need a degree of auditing and testing, to be sure, but formal proofs have never been a requirement since they aren't that practical. (emphasis mine) I was challenging this idea. Are systems for self-driving cars the only safety critical systems? What about Intel manufactured chips used in those same cars and flights and a gazillion other devices? You have an agenda to push and got called out on facts :) Have a good day. (Someone just went around down voting my other posts. Not you)
      - seanmcdirmid 11y ago
        I guess it depends on how you interpret "that", which I meant to refer to "requirement" (they are not practical enough to be a requirement). But I guess I should have been more clear in my sentence structure.
        cscurmudgeon 11y ago
        Still not clear but we will leave it here :) Btw, I use both deep learning and knowledge based systems in my work (but not formal verification) but don't like advertising that goes in AI by academics from all camps(don't want another AI winter).
        seanmcdirmid 11y ago
        Fair enough. I have no skin in this game since I'm a PL researcher...
- evvp137 11y ago
  I don't necessarily disagree with your points here, but for completeness you should note that DO-178B has been moving to DO-178C for a few years now, which includes references to formal methods for systems verification, specifically DO-333. Also, that paper by Denney is 10 years old, and some strides have been made since then to improve formal method tools for viable verification.

Not FUD at all. Pointing at a system doesn't provide any evidence that proofs are prevalent in industry. Check out: https://chess.eecs.berkeley.edu/hcssas/papers/Cleaveland-position-paper.pdf https://chess.eecs.berkeley.edu/hcssas/papers/Cleaveland-pos... > Although formal proofs of correctness are (rightly) touted as providing superior guarantees to those of testing, DO-178B makes no mention of formal methods, except in an Annex given over to techniques deemed not yet mature enough for certification purposes. Or http://ti.arc.nasa.gov/m/pub-archive/1023h/1023%20(Denney).pdf http://ti.arc.nasa.gov/m/pub-archive/1023h/1023%20(Denney).p...: > In principle, formal methods offer many advantages for aerospace software development: they can help to achieve ultra-high reliability, and they can be used to provide evidence of the reliability claims which can then be subjected to external scrutiny. However, despite years of research and many advances in the underlying formalisms of specification, semantics, and logic, formal methods are not much used in practice. In our opinion this is related to three major shortcomings. First, the application of formal methods is still expensive because they are labor- and knowledge-intensive. Second, they are difficult to scale up to complex systems because they are based on deep mathematical insights about the behavior of the systems (i.e., they rely on the “heroic proof”). Third, the proofs can be difficult to interpret, and typically stand in isolation from the original code. The situation will just get worse as we increasingly move away from hand written logic to machine learned logic. Now, there is probably a place for formal methods in this newer order, but it will take awhile for researchers to find it, and it is definitely not going to be at the level of verifying hand-encoded logic that doesn't exist.

cscurmudgeon 11y ago
I meant to point out formal verification is used in the industry quite a bit (not in aviation alone). 1. Replacing testing with formal verification at Intel (2009) http://link.springer.com/chapter/10.1007/978-3-642-02658-4_32 http://link.springer.com/chapter/10.1007/978-3-642-02658-4_3... 2. Fifteen years of formal property verification at Intel (2008) http://link.springer.com/chapter/10.1007/978-3-540-69850-0_8 http://link.springer.com/chapter/10.1007/978-3-540-69850-0_8 3. seL4: formal verification of an OS kernel http://dl.acm.org/citation.cfm?id=1629596 http://dl.acm.org/citation.cfm?id=1629596 There is such a big need that DARPA has even come up with a contest. http://www.darpa.mil/program/crowd-sourced-formal-verification http://www.darpa.mil/program/crowd-sourced-formal-verificati... I could go on, but I would rather not spend my time combating FUD and the general incivility here.
- seanmcdirmid 11y ago
  Formal verification is used a lot, but it is not a rule and definitely not a requirement by the FAA for aircraft certification. The idea that formal verification would be obviously necessary for the logic of a self-driving car is what was being challenged here. You could call that FUD, but you obviously have an agenda to push, I guess.
  - cscurmudgeon 11y ago
    > not a requirement by the FAA for aircraft certification. I never said that. Where did you get that? > Safety critical systems need a degree of auditing and testing, to be sure, but formal proofs have never been a requirement since they aren't that practical. (emphasis mine) I was challenging this idea. Are systems for self-driving cars the only safety critical systems? What about Intel manufactured chips used in those same cars and flights and a gazillion other devices? You have an agenda to push and got called out on facts :) Have a good day. (Someone just went around down voting my other posts. Not you)
    - seanmcdirmid 11y ago
      I guess it depends on how you interpret "that", which I meant to refer to "requirement" (they are not practical enough to be a requirement). But I guess I should have been more clear in my sentence structure.
      - cscurmudgeon 11y ago
        Still not clear but we will leave it here :) Btw, I use both deep learning and knowledge based systems in my work (but not formal verification) but don't like advertising that goes in AI by academics from all camps(don't want another AI winter).
        seanmcdirmid 11y ago
        Fair enough. I have no skin in this game since I'm a PL researcher...
evvp137 11y ago
I don't necessarily disagree with your points here, but for completeness you should note that DO-178B has been moving to DO-178C for a few years now, which includes references to formal methods for systems verification, specifically DO-333. Also, that paper by Denney is 10 years old, and some strides have been made since then to improve formal method tools for viable verification.