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

From: "Hallam-Baker, Phillip" <[email-masked]>
Date: Thu, 17 Nov 2005 08:56:14 -0800

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:[email-masked]] 
> Sent: Thursday, November 17, 2005 11:28 AM
> To: Hallam-Baker, Phillip
> Cc: Steve Crocker; Masataka Ohta; Yaakov Stein; 
> [email-masked]; 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
> [email-masked]
> 
> 
> 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: [email-masked] [mailto:[email-masked]] 
> On Behalf 
> >> Of Masataka Ohta
> >> Sent: Thursday, November 17, 2005 8:30 AM
> >> To: Yaakov Stein
> >> Cc: [email-masked]; 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
> >> [email-masked]
> >> https://www1.ietf.org/mailman/listinfo/ietf
> >>
> >>
> >
> > _______________________________________________
> > Ietf mailing list
> > [email-masked]
> > https://www1.ietf.org/mailman/listinfo/ietf
> 
> 
> 

_______________________________________________
Ietf mailing list
[email-masked]
https://www1.ietf.org/mailman/listinfo/ietf

---

From: Steve Crocker <[email-masked]>
Date: Thu, 17 Nov 2005 12:00:17 -0500

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
[email-masked]