[SystemSafety] proofs

[Gergely Buday]

On Fri, 23 Nov 2018 at 12:05, Martyn Thomas
<martyn at thomas-associates.co.uk> wrote:

> And, of course, the "descriptive data-sheet" should be as formal as
> possible so that it provides the basis for proofs and for warranties.
>
> But the software industry won't accept that formal specifications are
> necessary or that warranties are desirable, and their customers continue
> to let them get away with it.

Two points.

I have listened to a lecture about a legal constraint that might be
implemented in the US so that manufacturers cannot get away with
insecure software in e.g. routers. Everybody knows that customers are
ignorant about computer security but the government does not like this
and want to take action.

Second. The software industry is a wide range of things, and yes, for
the most part there will never be formal verification. What we are
talking about is high-end software, safety and security critical
software.

And there is a third: even hardware specifications are sometimes dubious.

- Gergely