[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[David MENTRÉ]

Dear Mr Jones,

Le 31/10/2019 à 20:53, Derek M Jones a écrit :
> A research group could lay out plans for the verification of all
> phases of a compiler.  Then for the work linked to they could
> say, "Hey we have done this part, next we are going to do..."
>
> I'm sure people would get behind a grand plan to verify everything
> associated with a compiler.

Yes, in fact from the machine architecture up to application level, this
is DeepSpec project: https://deepspec.org/main


> Claiming to have verified a compiler, when in fact the work only
> applies to parts of the code generator, is soap powder advertising. 

No, nowadays CompCert has proofs from the text parser to the code
generator! Even crucial parts of the assembling and linking process are
proved. And this is not "soap powder advertising", this is science. See
this paper https://hal.inria.fr/hal-01643290 for an overview, and
reference [11] within this paper for the proofs linking the text LR(1)
parser and C language semantics.

And yes, some parts are not proved, mainly pre-processing, and testing
is used there (again,see above paper for details).

We all know your skepticism regarding formal methods, and I agree with
you that between testing and proving approaches, one of them can be more
cost effective depending on use cases.

But they are industrial cases where formal methods are more efficient:

  * By Siemens and Alstom for more than 20 years to build CBTC and
    Switching systems
  * By Intel and AMD to verify floating point unit (since FDIV bug disaster)
  * By Airbus to check absence of run-time errors in Flight control
    software or correct floating-point behavior of their manually coded
    trigonometric library
  * By ARM to check well definition of ARMv8 architecture
  * By Amazon for their distributed protocols
  * By Gemalto to check correctness of some crucial smartcard elements
  * ...

If those companies are using formal methods, for some of them for more
than 20 years, it is not due to "soap powder advertising" but due to
real cost benefit over several projects.

To give just one example, safety critical data verification used for
example in CBTC projects, goes down from 1 month to 1 or 2 days
(compared to manual human review process), with rapid identification of
faulty data and strong confidence brought to the verification process.

On this list, we all know that safety does not reduce to one tool or one
approach, and formal methods is no better than test or review depending
on the project part. But correctly used formal methods can nowadays
really bring strong evidences, sometimes much more easily that with
classical test and review.

For me now the real question is: when is it cost effective to use formal
methods? Some formal methods are very heavy to put in place, so not cost
effective on the first but sometimes second or more project. I really
would like to have figures to determine when test or review is better,
for a given safety level, over the span of one or more projects.

Best regards,
D. Mentré


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191103/eb8b6425/attachment.html>