Hacker News Reader

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

View on HN

Which parts aren't automated?

Plenty of line still have drivers.

The only fully automated lines are 1 and 14.

The parts involving humans.

Interesting. Do you have any additional information on this?

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

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.

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 !

Reply on news.ycombinator.com