Comment by gregholmberg | Hacker News Reader

Top New Best Ask Show Jobs

Comment by gregholmberg | Hacker News Reader

Task: write a static analyzer to check primary control software for a new family of passenger airliners. [1]

Employer: Airbus.

Which language did the team choose for the analyzer? OCaml.

It is possible to write OCaml programs that are provably correct.

[0] "Caml language family" http://caml.inria.fr/

[1] "Success Stories" http://caml.inria.fr/about/successes.en.html

[2] "OCaml: a serious contender" http://caml.inria.fr/about/programming-contest.en.html

edit: clarity

It's worth pointing out that Airbus has a large presence in France and Ocaml is from a French research institution (INRIA). I highly doubt that's a coincidence.

Disclosure: Ocaml is my favorite language by far.

Objective Caml is not the only interesting thing to come out of there.

For a real eye opener, look through the current list of research topics at INRIA. I have (mis)spent hours reading the published papers and source code from some of their projects.

[0] "Equipes de recherche du centre Grenoble" http://www.inria.fr/recherches/equipes-de-recherche/recherch...

What language was the primary control software written in?

" ... a subset of the C programming language".

Er, I missed that footnote. Thanks.

I think you found the punch line.

Something like "if you want to write small, solid and safe control logic for an embedded system, you should generally use C. But if you want to prove it mathematically correct, you'll need to test it with software written in this obscure language from INRIA in Grenoble."

Reply on news.ycombinator.com