On Sunday, 14 May 2017 at 01:30:47 UTC, Jack Stouffer wrote:
It almost happened with Toyota. The auto industry has a C
coding convention for safety called MISRA C, and it was brought
up in court as to why Toyota's acceleration problems were
entirely their fault. You can bet this will be brought up again.
1. Changing language won't change this, for that you need
something that is formally proven (and even that assumes that the
requirements spec is correct).
I found this book from 2012 on industry use of formal methods
which seems to be available on Google Books:
https://books.google.no/books?id=E5sdDs00MuwC
2. What good does it do you to have your source code proven
formally correct if your compiler can contain bugs? To get around
that you need a formally verified compiler:
http://compcert.inria.fr/
So... We are back to C again.
