Brian,

>>>> I don't see the point about "current technology". We are talking about
>>>> stuff which is over a century, respectively nearly half a century, old.
>>
>> The theory might be, but the practice is very resource intensive.
> 
> Perhaps, but the MoD funded effort for an FD of SPARK was quite a bit
> of what would be needed.

Perhaps Rod can tell us what properties the FD of SPARK has been proved
to have.

> Also, if your 'model implementation' of C had been derived from a formal 
> definition,
> if could act as a check in the way I am advocating!

The C Model Implementation was originally written in Pascal and
then converted to C.

Given the availability of tools for C it was possible to check
a lot more of its properties than if it had been written in some
formal definition language (we are talking early 1990's here). 
www.knosof.co.uk/whoguard.html

However, whatever it had been written it, it would still be too big to
check for internal consistency even today.

-- 
Derek M. Jones                              tel: +44 (0) 1252 520 667
Knowledge Software Ltd                      mailto:derek@xxxxxx
Applications Standards Conformance Testing    http://www.knosof.co.uk