[SystemSafety] Number Theorist Fears All Published Math Is Wrong
Derek M Jones
derek at knosof.co.uk
Mon Dec 9 15:38:02 CET 2019
David,
> "The second contribution is a *soundness proof* for this algorithm,
> mechanized using
> the Coq proof assistant, guaranteeing with the highest confidence that
> if the
> validation of an automaton A against a grammar G succeeds, then the automa-
> ton A and the interpreter that executes it form a *correct* parser for
> G." (p. 2 of the paper, bold is mine)
There is no proof that the grammar G has any connection to C, or
any other language.
>> Large companies are involved in a wide range of activities.
>> Please provide links to sources showing real cost benefit savings.
>
> One link (bold is mine) because I don't have much time:
>
> B in Large-Scale Projects: The Canarsie Line CBTC Experience
> https://link.springer.com/chapter/10.1007/11955757_21
Thanks for this.
> "Beyond the technological challenge of using such a complex formal
> method in an industrial context, it is now clear for us that *building
> software using B is not more expensive than using conventional methods*.
> Better, due to our experience in using this method, we can assert that
> *using B is cheaper when considering the whole development process*
> (from specification to validation and sometimes certification)."
People use technique B, and then assert that they were right to choose
it because they think it was the best choice.
> "In fact, the onboard vital software was carried out with a team of 4
> persons
...
> and does not require a pool of experts in formal methods."
Details about what the team, but no comparison with anything else.
>> A cost benefit analysis needs to include the startup costs.
>> How much did it cost to create the tooling to automate the process?
>
> Tools like Atelier B (to do B Method formal development) is Component Of
> The Shelf (COTS). Last time I looked, Atelier B was at ~5k€/seat/year.
The cost of the tool is one (often small) component of startup costs.
--
Derek M. Jones Software analysis
tel: +44 (0)1252 520667 blog:shape-of-code.coding-guidelines.com
More information about the systemsafety
mailing list