[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[Derek M Jones]

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