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