![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
Steve
Steve Crocker steve at shinkuro.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.com] Sent: Thursday, November 17, 2005 11:28 AM To: Hallam-Baker, Phillip Cc: Steve Crocker; Masataka Ohta; Yaakov Stein; ietf at ietf.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.com
On Nov 17, 2005, at 10:09 AM, Hallam-Baker, Phillip wrote:
If we want to enforce simpler, more accurate design thebest way to doOn Behalfthis 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.org [mailto:ietf-bounces at ietf.org]characters areOf Masataka Ohta Sent: Thursday, November 17, 2005 8:30 AM To: Yaakov Stein Cc: ietf at ietf.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 ASCIIforbidden.
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.org https://www1.ietf.org/mailman/listinfo/ietf
_______________________________________________ Ietf mailing list Ietf at ietf.org https://www1.ietf.org/mailman/listinfo/ietf
_______________________________________________ Ietf mailing list Ietf at ietf.org https://www1.ietf.org/mailman/listinfo/ietf
Note Well: Messages sent to this mailing list are the opinions of the senders and do not imply endorsement by the IETF.