[SystemSafety] Fetzer

[Derek M Jones]

David,

Proponents of particular languages invariably claim 'magical'
properties for the language.  No evidence is ever provided, and
apart from a handful of exceptions, no experimental evidence
exists.  It's all personal opinion.

> 1. Specification languages are designed with *safety in mind*, unlike
> most programming languages. So the error rate for the specification per
> 1000 lines is likely to be lower than for the program.

Unsubstantiated marketing claim.

> 2. A specification is (or should be) *much shorter* and less complex
> than the program that implements it. So again, the specification should
> contain many fewer errors.

Unsubstantiated marketing claim.

> 3. Specifications can themselves be verified formally to some extent by
> including redundancy. In Escher C/C++ Verifier, we do this by means of

How people love that term "verified formally"; what you mean is that
consistency checks can be made.

Such consistency can be made for programs written in any language.

> I might add that constructing a formal specification it itself very
> helpful in exposing ambiguity and uncertainty in the user's requirements.

Creating two implementations of a system in two different languages, or
by two different groups, has always been helpful in exposing ambiguity
and uncertainty in the user's requirements.
It is the basis of N-version programming.

> 
> David Crocker, Escher Technologies Ltd.
> http://www.eschertech.com
> Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486
> 
> On 19/06/2019 15:19, Derek M Jones wrote:
>> David,
>>
>>> nobody constructs program proofs by hand these days, except perhaps in
>>> academia. Formal proofs of programs are always constructed either
>>> completely automatically, or in a few cases using an interactive theorem
>>> prover.
>>
>> This approach is essential N-version programming, with N=2.
>>
>> Two programs get written, one is nominated to be the specification,
>> and a tool checks that the behavior of the two programs are consistent
>> with each other.
>>
>> The correctness argument relies on a verbal slight of hand.  The
>> program nominated to be the specification is deemed to be correct,
>> because it's the specification.  If the second program has consistent
>> behavior, compared to the 'specification', then it's said to be correct.
>>
>>> So the important question is: what is the error rate of
>>> machine-constructed program proofs, produced by whatever tool is used to
>>> generate them. I think this is akin to asking what is the rate of code
>>
>> There is a lot more to consider than the error rate of the tool.
>>
>> Particular tools are based on particular mathematical formalisms.  Which
>> means they are not capable of detecting inconsistencies of a kind not
>> supported by the formalism used, i.e., they look for a specific kind
>> of inconsistency.
>>
>> As with all N-version solutions, the same incorrect behavior can occur
>> in both programs being compared.
>>
>>> David Crocker, Escher Technologies Ltd.
>>> http://www.eschertech.com
>>> Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486
>>>
>>> On 19/06/2019 13:54, Derek M Jones wrote:
>>>> David,
>>>>
>>>> The idea that software can be proved correct is based on the
>>>> assumption that mathematics is always correct.
>>>>
>>>> Plenty of mistakes get made in so called mathematical proofs.
>>>> In some cases theorems are given with only an outline of a proof.
>>>>
>>>> And of course, a lot more people are running code, than checking
>>>> mathematical proofs.  So more mistakes get found in code than
>>>> mathematics.
>>>>
>>>> The continuing belief that mathematics can be used for proving
>>>> software correct should be a fertile topic for social scientists
>>>> and anthropologists, no need to visit 'primitive' tribes to
>>>> find strange ideas, they are here under their noses.
>>>>
>>>> https://shape-of-code.coding-guidelines.com/2013/11/17/what-is-the-error-rate-for-published-mathematical-proofs/
>>>>
>>>>
>>>>
>>>> https://shape-of-code.coding-guidelines.com/2018/02/19/mathematical-proofs-contain-faults-just-like-software/
>>>>
>>>>
>>>>
>>> _______________________________________________
>>> The System Safety Mailing List
>>> systemsafety at TechFak.Uni-Bielefeld.DE
>>> Manage your subscription:
>>> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>>>
>>
> 
> 
> 
> _______________________________________________
> 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