Joshua D. Guttman writes:
 > 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. 

There's a joke around in the formal methods community: ``would you
prefer to get on a plane whose software has been proved correct or
has been tested?''

More seriously, I heard a similar remark from a French company which
formally verified the embedded code of an automatic subway line (using
the B method). They explained that, after the verification had been
completed, the unit phase was not suppressed, but greatly reduced.

-- 
Jean-Christophe