On 25/09/17 16:49, Emanuel Berg wrote:
> Mario Castelán Castro wrote:
> 
>> This is the prevalent attitude among
>> programmers
> 
> Perhaps because it makes sense? It is known as
> "conventional wisdom".
> 
>> we are showered by an endless stream of
>> security patches and bug fixes.
> 
> Yes, and what is the problem with that?

Obviously each such fix is evidence that a security vulnerability or
another defect existed in the first place. A shower of fixes means that
bugs are extremely prevalent in software. Otherwise it would have been
impossible to sustain this tremendous bug discovery rate for years
(check any web front end to the CVE database for details).

Thus it is clear that the mainstream approach to writing software is
failing to delivers reliable software. That is why we have the need for
an alternative. Among all possible approaches, *only* formal testing has
the possibility of virtually eliminating software defects.

Note that errors in the model of the environment (as in the paper
previously mentioned in this conversation) are not a *consequence* of
formal verification. This is just a symptom, and moreover it is routine
in non-formally verified software (i.e.: the developers make assumptions
about the environment that will not always be met).

For example, in Linux[1] they use the -fno-strict-pointer-aliasing
compiler flag which is just a way to shove under the rug the problem of
some incorrect assumptions they make about the semantics of C. This is
an error of the implicit model of the environment. It is not stated in
formal logic, but it is an error nonetheless.

Formal verification provide a solution for this problem: If the low
level software that makes up the environment for high level software has
a formal specification, then the possibility of errors in the model of
the environment can be eliminated by using the pre-existing formal model
of the environment.

[1] I mean Linux, the *kernel* used in GNU/Linux and other OS.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan