Fantastic exchange from DConf

[Ola Fosheim Grøstad via Digitalmars-d]

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.