Hacker News Reader

Comment by fuklief | Hacker News Reader

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

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?

Miscompilation issues means bugs in the compiler causing incorrect assembly to be generated.

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)

Check out "Finding and Understanding Bugs in C Compilers": 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/.

Thank you, that paper seems to be surprisingly easy to read (being an academic paper that is).

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.

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

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.

>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?

> 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.

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.

...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.

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 :-)

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

Reply on news.ycombinator.com