4 ms·

The Paris subwway network is partially automated. The software is written in OCaml, and mathematically proven correct using Coq.

• sitkack 12y ago
  Which parts aren't automated?
  • _qhtn 12y ago
    The parts involving humans.
  • brohee 12y ago
    Plenty of line still have drivers. The only fully automated lines are 1 and 14.
• donquichotte 12y ago
  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 !