4 ms·

Coq is also used in industry, in particular by Airbus with the CompCert C compiler.

by fuklief 11y ago

pron 11y ago
Do Airbus engineers write Coq specifications or just use CompCert (a C compiler formally verified with Coq in academia)?
- deleted 11y ago
  [deleted]
- nmrm2 11y ago
  This distinction is disingenious (edit: I probably mean spurious). The number of people in industry who use either tool is incredibly small and is likely to remain so; developers spend 20-50% of their time on test suites and STILL don't feel it's cost-effective to write down formal specs, even in TLA+-style specifications. What matters is that important libraries and frameworks can be verified, not that everyone and his brother can use formal methods for every WordPress website they churn out.
  - pron 11y ago
    > The number of people in industry who use either tool is incredibly small and is likely to remain so I agree, but I see some chance of TLA+ of getting wide(r) adoption, precisely because it is rather easy to learn and uses math that most engineers are already familiar with. Also, it allows gradual verification: specification -> model-checking -> proof (with each additional step being completely optional) > not that everyone and his brother can use formal methods for every WordPress website they churn out. I don't know about WordPress websites, but Amazon engineers do use TLA+ to specify many (most?) AWS services.
    - nmrm2 11y ago
      My point was just that formal methods can have a tremendous positive impact even if academics are the only ones using them, as long as the output from those efforts do get used. So I'm not sure distinguishing between "using formally verified software" and "using a formal methods tool directly" is a helpful distinction when measuring industrial impact. Also, formalizing architectural properties for the world's most popular cloud service is probably even rarer a task than formalizing language specifications.
  - jessaustin 11y ago
    ...disingenious. English usage note: if the word you meant to use was "disingenuous", I would suggest "spurious" instead, as it expresses similar feelings about "this distinction", without also attributing unsavory motives to 'pron.
    - ScottBurson 11y ago
      Hey, I like this word "disingenious". I think it could mean "a bad idea being promulgated to displace (what the speaker considers) a much better idea". We need a word for that :-)
  - eli_gottlieb 11y ago
    >The number of people in industry who use either tool is incredibly small and is likely to remain so; developers spend 20-50% of their time on test suites and STILL don't feel it's cost-effective to write down formal specs, even in TLA+-style specifications. How many zero-day security flaws have to occur in core infrastructure like, for instance, OpenSSH before the laziness of engineers about learning "academic" tools stops being a cost-effective excuse not to use formal methods?
- pascal_cuoq 11y ago
  Both. “They” (and by they I do not necessarily imply a large number of engineers at Airbus, but some people who are engineers at Airbus) use CompCert and “they” also use Coq in order to finish up the correctness arguments for part of the properties that part of the software is supposed to have: https://www.lri.fr/~marche/M2-TIP-Airbus.pdf https://www.lri.fr/~marche/M2-TIP-Airbus.pdf
feider 11y ago
From CompCert site: "What sets CompCert C apart from any other production compiler, is that it is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues." I'm not very into C language - what are these miscompilation issues? What is the practical impact that CompCert C brings?
- witty_username 11y ago
  Miscompilation issues means bugs in the compiler causing incorrect assembly to be generated.
  - feider 11y ago
    I understood that. Sorry if my question was bit unclear. What I wanted to know was _specifically_ what these bugs are / what causes them / what is practical impact (i.e. probability of application crashing or other serious event due to use of GCC etc)
    - sanxiyn 11y ago
      Check out "Finding and Understanding Bugs in C Compilers": http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf. The paper explains what-is-bug/what-causes-it/what-is-impact for selected bugs. Complete list of 282 compiler bugs found (79 GCC, 203 LLVM) is also available online: http://embed.cs.utah.edu/csmith/ http://embed.cs.utah.edu/csmith/.
      - feider 11y ago
        Thank you, that paper seems to be surprisingly easy to read (being an academic paper that is).
    - nickpsecurity 11y ago
      Especially see the CompCert section on page 6 of the Csmith PDF to see what a difference formal verification made. Note that compilers don't have to go that far: typed, functional, thoroughly-tested code in something like Ocaml or Haskell can achieve 80-90% of that quality with relatively little effort. Hence, why I promote rewriting and further extending things like LLVM in languages like ML, Ada, or Eiffel that support advanced checks.

Coq is also used in industry, in particular by Airbus with the CompCert C compiler.

by fuklief 11y ago

Coq is also used in industry, in particular by Airbus with the CompCert C compiler.

pron 11y ago

Do Airbus engineers write Coq specifications or just use CompCert (a C compiler formally verified with Coq in academia)?

deleted 11y ago
[deleted]
nmrm2 11y ago
This distinction is disingenious (edit: I probably mean spurious). The number of people in industry who use either tool is incredibly small and is likely to remain so; developers spend 20-50% of their time on test suites and STILL don't feel it's cost-effective to write down formal specs, even in TLA+-style specifications. What matters is that important libraries and frameworks can be verified, not that everyone and his brother can use formal methods for every WordPress website they churn out.
- pron 11y ago
  > The number of people in industry who use either tool is incredibly small and is likely to remain so I agree, but I see some chance of TLA+ of getting wide(r) adoption, precisely because it is rather easy to learn and uses math that most engineers are already familiar with. Also, it allows gradual verification: specification -> model-checking -> proof (with each additional step being completely optional) > not that everyone and his brother can use formal methods for every WordPress website they churn out. I don't know about WordPress websites, but Amazon engineers do use TLA+ to specify many (most?) AWS services.
  - nmrm2 11y ago
    My point was just that formal methods can have a tremendous positive impact even if academics are the only ones using them, as long as the output from those efforts do get used. So I'm not sure distinguishing between "using formally verified software" and "using a formal methods tool directly" is a helpful distinction when measuring industrial impact. Also, formalizing architectural properties for the world's most popular cloud service is probably even rarer a task than formalizing language specifications.
- jessaustin 11y ago
  ...disingenious. English usage note: if the word you meant to use was "disingenuous", I would suggest "spurious" instead, as it expresses similar feelings about "this distinction", without also attributing unsavory motives to 'pron.
  - ScottBurson 11y ago
    Hey, I like this word "disingenious". I think it could mean "a bad idea being promulgated to displace (what the speaker considers) a much better idea". We need a word for that :-)
- eli_gottlieb 11y ago
  >The number of people in industry who use either tool is incredibly small and is likely to remain so; developers spend 20-50% of their time on test suites and STILL don't feel it's cost-effective to write down formal specs, even in TLA+-style specifications. How many zero-day security flaws have to occur in core infrastructure like, for instance, OpenSSH before the laziness of engineers about learning "academic" tools stops being a cost-effective excuse not to use formal methods?
pascal_cuoq 11y ago
Both. “They” (and by they I do not necessarily imply a large number of engineers at Airbus, but some people who are engineers at Airbus) use CompCert and “they” also use Coq in order to finish up the correctness arguments for part of the properties that part of the software is supposed to have: https://www.lri.fr/~marche/M2-TIP-Airbus.pdf https://www.lri.fr/~marche/M2-TIP-Airbus.pdf

feider 11y ago

From CompCert site: "What sets CompCert C apart from any other production compiler, is that it is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues." I'm not very into C language - what are these miscompilation issues? What is the practical impact that CompCert C brings?

witty_username 11y ago
Miscompilation issues means bugs in the compiler causing incorrect assembly to be generated.
- feider 11y ago
  I understood that. Sorry if my question was bit unclear. What I wanted to know was _specifically_ what these bugs are / what causes them / what is practical impact (i.e. probability of application crashing or other serious event due to use of GCC etc)
  - sanxiyn 11y ago
    Check out "Finding and Understanding Bugs in C Compilers": http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf. The paper explains what-is-bug/what-causes-it/what-is-impact for selected bugs. Complete list of 282 compiler bugs found (79 GCC, 203 LLVM) is also available online: http://embed.cs.utah.edu/csmith/ http://embed.cs.utah.edu/csmith/.
    - feider 11y ago
      Thank you, that paper seems to be surprisingly easy to read (being an academic paper that is).
  - nickpsecurity 11y ago
    Especially see the CompCert section on page 6 of the Csmith PDF to see what a difference formal verification made. Note that compilers don't have to go that far: typed, functional, thoroughly-tested code in something like Ocaml or Haskell can achieve 80-90% of that quality with relatively little effort. Hence, why I promote rewriting and further extending things like LLVM in languages like ML, Ada, or Eiffel that support advanced checks.