Subject: Re: SDL Demo and ITU CD Q&A

From: Vernon Schryver <[email-masked]>
Date: Fri, 7 Dec 2001 16:02:11 -0700 (MST)

> From: Keith Moore <[email-masked]>

> ...
> But I do think that IETF standards could benefit from more formal
> description languages for protocols. So I thank ITU folks for their
> efforts to show this to us. I'll be interested to see what SDL looks 
> like.  
> ...

Oh, golly, just what we need, more of the "put it into this 
language/checker/verifier/magic box and it will come out perfect"
stuff that has been so productive for the last 25 or 30 years in general
computer programming and for the last 15 years for network protocols.

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.

Vernon Schryver    [email-masked]

---

From: Robert Moskowitz <[email-masked]>
Date: Sun, 09 Dec 2001 14:07:52 -0500

>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....