RE: Theoretical question about vulnerabilities

["David Crocker" <dcrocker () eschertech com>]

der Mouse wrote:

> >
Basically, the same arguments usually made for any higher-level langauge versus
a corresponding lower-level language: machine versus assembly, assembly versus
C, C versus Lisp, etc.

And I daresay that it provides at least vaguely the same advantages and
disadvantages as for most of the higher/lower level comparisons, too. But it is
hardly the panacea that "proving the program correct" makes it sound like.  As
someone (who? I forget) is said to have said, "Beware, I have only proven this
program correct, not tested it".
<<

There are actually 2 separate issues here:

1. There are tools (such as Perfect Developer) that allow you to write
specifications and will then generate all or most of the code automatically.
This is the "VHLL" situation you are talking about. This approach increases both
reliability and productivity, because the software developer has less to write
and the specification is much closer to the problem than the code needed to
implement it.

2. Proving programs correct with respect to some specification (including
implied specifications such as absence of buffer overflow). I defend the use of
the term "proof" here, provided that the software developer can amass a
reasonable body of evidence that the proof process is sound. Possible evidence
includes: testing the software thoroughly and finding ZERO bugs; checking the
proofs using independent proof checking software; manually checking a selection
of the proofs; and using similar techniques to prove the proof-generating
software correct, whilst taking care to avoid circular arguments. Of course, one
could write a buggy prover, in the same way that one can write a buggy compiler;
but just as the compilers from the best suppliers mature until they are
considered trustworthy by their customers, so can proof tools gain in maturity
and stature. Tools such as SPARK and Atelier B have already reached this level
of trust, and I am confident that Perfect Developer will be equally trusted
after a few more years commercial usage. BTW it is by no means unknown for a
body of mathematicians to consider a theorem proven and then for a mistake in
the proof to be found (e.g. the early "proofs" of the four-colour theorem); so I
really don't think that proofs that are manually derived and manually checked
are necessarily better than computer-generated proofs.

David Crocker, Escher Technologies Ltd.
Consultancy, contracting and tools for dependable software development
www.eschertech.com