Hacker News new | ask | show | jobs
by fuklief 2701 days ago
Are you sure on that? It was B method they used afaik.
2 comments
cpeterso 2701 days ago
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

link
nestorD 2700 days ago
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...

link