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

From: "Hallam-Baker, Phillip" <[email-masked]>
Date: Thu, 17 Nov 2005 07:09:16 -0800

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

---

From: Steve Crocker <[email-masked]>
Date: Thu, 17 Nov 2005 11:28:01 -0500

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]

---

From: Frank Ellermann <[email-masked]>
Date: Thu, 17 Nov 2005 17:59:56 +0100

Steve Crocker wrote:

> Just something simple and instructive to make your point.
> And in light of the other issues being discussed, don't

Do you expect Phil's reply before 2007 ?  There were some
really nice SDL-tools about fifteen years ago.  Bye, Frank

---

From: Harald Tveit Alvestrand <[email-masked]>
Date: Thu, 17 Nov 2005 10:34:41 -0800

I remember that when the ITU-T was pushing for more use of formal tools in 
its IETF cooperation, around the London timeframe (2001), one person wrote 
a formal definition of OSPF in one of their formalisms.

I don't remember if he found any problems in the spec based on that 
exercise, but people more intimately connected to this problem space may 
remember more.

             Harald

                    Harald

---

From: Cameron Kerr <[email-masked]>
Date: Sat, 19 Nov 2005 20:19:33 +1300

Have any RFC protocols been specified using formal tools for their  
message interaction? I know a few use ASN.1, such as SNMP and LDAP,  
which have come from the ITU-T, but that's only for specifying the  
syntax (abstract or transfer), not the interaction of messages.

 From what I've been able to tell, the only mention to SDL in the  
RFCs is in relation to Simple Data Link. I'm currently just learning  
about ASN.1, so I don't know much about this space at the moment.

On 18/11/2005, at 5:28 AM, Steve Crocker wrote:

> mind the proof of correctness; that can come later.  (And with it  
> an extended discussion of the underlying logical system, the formal  
> 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]
>
>

-- 
• Cameron Kerr  • ✉ [email-masked] • •
• Telecommunications Teaching Fellow & SysAdmin •
• ✎ http://humbledown.org/blog/ • ✆ 021 4117 644 •