4 ms·

Interesting. Do you have any additional information on this?

• monort 12y ago
  It seems to be not OCaml: First real success was Meteor line 14 driverless metro in Paris: Over 110 000 lines of B models were written, generating 86 000 lines of Ada. No bugs were detected after the proofs, neither at the functional validation, at the integration validation, at on-site test, nor since the metro lines operate (October 1998). The safety-critical software is still in version 1.0 in year 2007, without any bug detected so far. From: http://rodin.cs.ncl.ac.uk/Publications/fm_sc_rs_v2.pdf http://rodin.cs.ncl.ac.uk/Publications/fm_sc_rs_v2.pdf
  • Artemis2 12y ago
    Pure languages are also great for this kind of thing, because of the lack of side-effects (aka Haskell's moto). OCaml manages its imperative parts in a way that isn't as good had Haskell does, but it's probably possible to get a very clean code that is mostly pure, allowing a mathematical proof of safety.
  • malka 12y ago
    My bad. I heard from this from a friend that used to work at the RATP (Paris Subway). Thanks you for the link, very instructive !