... but they use OCaml to prove that there are no run-time errors (RTE) in their code :-) http://www.astree.ens.fr/ http://www.astree.ens.fr/ "In Nov. 2003, A

... but they use OCaml to prove that there are no run-time errors (RTE) in their code :-) http://www.astree.ens.fr/ http://www.astree.ens.fr/ "In Nov. 2003, ASTRÉE was able to prove completely automatically the absence of any RTE in the primary flight control software of the Airbus A340 fly-by-wire system, a program of 132,000 lines of C. [...] From Jan. 2004 on, ASTRÉE was extended to analyze the electric flight control codes then in development and test for the A380 series."