Hacker News Reader

The exemple I was given while studying the subject is that the sofware for the driverless metro line 14 in Paris has been proven in Coq.

View on HN

Are you sure on that? It was B method they used afaik.

Wikipedia says B-Method. Parts of the train control system use OpenVMS!

https://en.wikipedia.org/wiki/Paris_M%C3%A9tro_Line_14

https://en.wikipedia.org/wiki/B-Method

I was told Coq but, after some checking, I can only find the B method indeed. However I did find a paper mixing both ([0]) : using Coq to prove the more complex proofs generated by atelier B. So it might have been both.

[0] https://perso.crans.org/cauderlier/org/art%253A10.1007%252Fs...

Reply on news.ycombinator.com