[SystemSafety] A small taste of what we're up against

[Peter Bernard Ladkin]

On 2018-10-24 13:11 , Derek M Jones wrote:
> 
> 
>> - it increases the productivity and reduces the introduction of defects in the sources.
> There is no evidence for any of these claims.
There is in fact a large body of, to most of us, convincing evidence of such claims.

My personally most convincing evidence was accumulated writing the SW for my PhD thesis. It
implemented an interval-real-time calculator. I spent a few months writing/unit-testing it alone.
The system integrator integrated it into a larger collection of SW called the Project Management
Assistant (part of Rome ADC's KBSA project) in a couple of hours (and found a boundary condition I
had overlooked). It then ran from the next day on a demo at AAAI86, and proceeded to run for a
number of years as quasi-"production" software in the PMA for the client, without a single
additional bug report.

That was all written in a wonderful language called REFINE, which had both procedural and
declarative constructs and was wonderfully easy to read (in terms of the intended meaning). And
using the declarative constructs you could write the intended semantics into the pre- and
post-conditions of the functions, which made Hoare-style verification part of the programming task,
as it is in SPARK, for example.

However:
* there was no formal semantics
* there had been no formal verification of the compiler
* the target language was that very favorite of SW developers everywhere, LISP

The last point meant that there was a limited, and ultimately no, future for the technology. And no
one would pay for a verified implementation in a more SW-development-usual language. I am not sure
it lasted out the 20thC.

PBL

Prof. Peter Bernard Ladkin, Bielefeld, Germany
MoreInCommon
Je suis Charlie
Tel+msg +49 (0)521 880 7319  www.rvs-bi.de





-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20181024/9639faa8/attachment.sig>