RE: Diagrams (Was RFCs should be distributed in XML)

The description was sufficiently complete to allow running code to be
compiled from the formal specification. 


It certainly does save time when used by someone who has the necessary
experience to work at a very high level of abstraction. The problem is
that it is very hard to persuade others to then maintain the generated
code as this is not a mainstream coding technique. We can get people to
use Lex and Yacc for specific projects but the idea of developing a tool
for the project is something that is not very popular outside MIT and
the like.

If you read Kernighan and Plaugher's book on software tools you will see
that this approach did play an important role in the early development
of Unix. But what has tended to happen since is that people have taken
the specific tools developed rather than adopt the approach.

-----Original Message-----
From: Steve Crocker [mailto:steve(_at_)shinkuro(_dot_)com] 
Sent: Thursday, November 17, 2005 12:00 PM
To: Hallam-Baker, Phillip
Cc: Steve Crocker; Masataka Ohta; Yaakov Stein; 
ietf(_at_)ietf(_dot_)org; Stewart Bryant
Subject: Re: Diagrams (Was RFCs should be distributed in XML)

Well, even if you choose your formalism first and then use 
that to guide the development and specification of the 
protocols, the challenge still stands.  The operative word in 
your description is "portions."  Does the technique cover 
enough of the protocol to be useful and does it wind up 
adding or saving time, work, errors, etc?

Steve

Steve Crocker
steve(_at_)shinkuro(_dot_)com

On Nov 17, 2005, at 11:56 AM, Hallam-Baker, Phillip wrote:

There is a way, develop a highly targetted formalism for

the specific

problem.

This is hard to apply to existing specs because they tend to be 
inconsistent. If you are required to apply a formalism you

have to be

much more consistent in your design approach.

I did this for the finite state portions of FTP, NNTP and

SMTP in 1993

when I was working on HTTP. With HTTP at the time there was

not a lot

of state.

-----Original Message-----
From: Steve Crocker [mailto:steve(_at_)shinkuro(_dot_)com]
Sent: Thursday, November 17, 2005 11:28 AM
To: Hallam-Baker, Phillip
Cc: Steve Crocker; Masataka Ohta; Yaakov Stein; ietf(_at_)ietf(_dot_)org; 
Stewart Bryant
Subject: Re: Diagrams (Was RFCs should be distributed in XML)

Phillip,

I spent a large fraction of my professional life in

pursuit of this

alluring and seemingly simple goal.  Here's a small
challenge: Take
*any* IETF protocol and write down the formal specification.
Never mind the proof of correctness; that can come later.
(And with it an extended discussion of the underlying

logical system,

the formal system for representing the protocol specification, and 
the proof system you have in mind for carrying out the proof.)  Of 
course, the formal specification will have to be readable and 
understandable to the general population, and there will have to 
ready agreement that it does embody the desired properties.  Pick 
something simple.
Perhaps IP?  Feel free to leave out messy details like performance 
issues if you wish.  Just something simple and instructive to make 
your point.  And in light of the other issues being

discussed, don't

feel constrained to use ASCII.
Use any notation and tools you like.

Steve



Steve Crocker
steve(_at_)shinkuro(_dot_)com


On Nov 17, 2005, at 10:09 AM, Hallam-Baker, Phillip wrote:

If we want to enforce simpler, more accurate design the

best way to do

this would be to require a formal proof of correctness before 
accepting a specification.

Requiring people to use 1960s technology is not a way to achieve 
simplicity.

-----Original Message-----
From: ietf-bounces(_at_)ietf(_dot_)org 
[mailto:ietf-bounces(_at_)ietf(_dot_)org]

On Behalf

Of Masataka Ohta
Sent: Thursday, November 17, 2005 8:30 AM
To: Yaakov Stein
Cc: ietf(_at_)ietf(_dot_)org; Stewart Bryant
Subject: Re: Diagrams (Was RFCs should be distributed in XML)

Yaakov Stein wrote:

It's good that protocols needing more than 72 ASCII

characters are

forbidden.

Just imagine what elegantly simple protocols we would

have if we

required the descriptions to be in Morse code.


Good idea.

It's a better approach to enforce much simpler protocols.

                                         Masataka Ohta


_______________________________________________
Ietf mailing list
Ietf(_at_)ietf(_dot_)org
https://www1.ietf.org/mailman/listinfo/ietf


_______________________________________________
Ietf mailing list
Ietf(_at_)ietf(_dot_)org
https://www1.ietf.org/mailman/listinfo/ietf


_______________________________________________
Ietf mailing list
Ietf(_at_)ietf(_dot_)org
https://www1.ietf.org/mailman/listinfo/ietf