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

[Derek M Jones]

Peter,

> My personally most convincing evidence was accumulated writing the SW for my PhD thesis. It

A rambling anecdote containing no evidence.

Were you hoping that readers will have forgotten the statement at the
top, by the time they had reached the bottom (assuming they had not
given up before the end)?


> 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
> 
> 
> 
> 
> 
> 
> 
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> 

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com