4 ms·

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 cho

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/ http://caml.inria.fr/ [1] "Success Stories" http://caml.inria.fr/about/successes.en.html http://caml.inria.fr/about/successes.en.html [2] "OCaml: a serious contender" http://caml.inria.fr/about/programming-contest.en.html http://caml.inria.fr/about/programming-contest.en.html edit: clarity

tjr 14y ago
What language was the primary control software written in?
- gregholmberg 14y ago
  " ... a subset of the C programming language".
  - tjr 14y ago
    Er, I missed that footnote. Thanks.
    - gregholmberg 14y ago
      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."
      - deleted 14y ago
        [deleted]
pgroves 14y ago
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.
- gregholmberg 14y ago
  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/rechercher-une-equipe http://www.inria.fr/recherches/equipes-de-recherche/recherch...

tjr 14y ago

What language was the primary control software written in?

gregholmberg 14y ago
" ... a subset of the C programming language".
- tjr 14y ago
  Er, I missed that footnote. Thanks.
  - gregholmberg 14y ago
    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."
    - deleted 14y ago
      [deleted]

pgroves 14y ago

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.

gregholmberg 14y ago
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/rechercher-une-equipe http://www.inria.fr/recherches/equipes-de-recherche/recherch...