[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[Derek M Jones]

Gergely,

> what do you offer than as an alternative?

An alternative to what?

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.

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

There has been some work on a small part of the front end; not
so much soap powder advertising for this work (I guess too much
advertising would lead people to question previous claims).

> - Gergely
> 
> Derek M Jones <derek at knosof.co.uk> ezt írta (időpont: 2019. okt. 30., Sze
> 22:00):
> 
>> Gergely,
>>
>>> for non-malicious, even correct compilers check CompCert and CakeML.
>>
>> Any discussion of formal methods eventually mentions soap
>> powder advertising:
>>
>> http://shape-of-code.coding-guidelines.com/2013/03/10/verified-compilers-and-soap-powder-advertising/
>>
>>
>> --
>> Derek M. Jones           Software analysis
>> tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com
>> _______________________________________________
>> The System Safety Mailing List
>> systemsafety at TechFak.Uni-Bielefeld.DE
>> Manage your subscription:
>> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>>
> 

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com