Re: SDL Demo and ITU CD Q&A

[Robert Moskowitz <rgm-ietf at htt-consult.com>]

At 04:02 PM 12/7/2001 -0700, Vernon Schryver wrote:

> I'm sorry for being so rude, but if you've been around a while, you've
> seen and should have learned from the final outcomes of design processes
> (including some for network protocols) that overtly involved formal
> "methodologies."  It's not that formal thinking is not useful and valuable,
> because it is.  Instead it seems that formal mechansms are always sold
> as a substitute for design skill and talent, but end up consuming a lot
> of both that should have been spent on designing the nominal product,
> while the nominal product comes out as OSI 87 layer cake.
>
> Now of course, I'll be told I'm all wrong, that the Space Shuttle
> software is a wonderful example of how to do things right, that the
> next use of a correctness prover will be for something really impressive
> like a gcd algorithm that handles negative numbers, that XTP didn't
> fail in the marketplace on its own defects, and similar stories.

Vern, I would say you are right but for a different reason.

Almost all formal exercises like this fail to take into account those that 
live outside the rules.

In the Space Shuttle, there was little concern about onboard viruses.

I have been told that TCP was extensively modeled and reviewed.  But look 
at the attacks that came later.

Formal languages are nice but they are traps themselves as they limit the 
allowed thinking by developers.  Look at Common Criteria as yet another 
example....