Re: [Caml-list] Programming with correctness guarantees

["Joshua D. Guttman" <guttman@mitre.org>]

oleg@pobox.com writes:

>   I remember reading somewhere that after a division of
>   Siemens applied this technique to a high assurance
>   project, they noted an exhilarating feeling of being
>   able to program without unit tests. The code was correct
>   by construction.

This seems really frightening.  Don't the unit tests also
serve another purpose, namely to confirm that the formal
model of the software environment is correct?

That is, that all of the libraries you're linking against
(and the compiler itself) are behaving in a way that matches
the expectations you formalized?

As well as a concrete confirmation that the formalized ideas
match correctly against what you really wanted in specific
instances:  the formal insight of human beings is imperfect.
(:-) 

I hope that the words "exhilarating feeling" were meant to
indicate that they didn't really do this, but had the
impression that they could *almost* do so.  

You don't want to lose contact with the real world
constraints when programming in a formally supported way.

I suppose that this doesn't really have much to do with
OCaml; apologies.  

        Joshua 


-- 
	Joshua D. Guttman 
	The MITRE Corporation