Like live polio vaccine there tends to be a prophilactic effect that has wider application. Although formal methods were not used in the design of Java and were not part of the design of C# as far as I am aware, both languages were designed after the field of software language development had spent a great deal of time working on ways to prove the correctness of the language features they incorporate. The principle advantage to formal methods thus far appears to be pedagogical, once you have tried to prove large stringy ugly systems correct you start to see more of an advantage to starting with something simpler. I am sure that there are other people who work on IETF protocols that go through the process of producing proof sketches as part of their design work. As for sharing them more widely, lets start with the low hanging fruit like using clear typography... > -----Original Message----- > From: ietf-bounces@xxxxxxxx [mailto:ietf-bounces@xxxxxxxx] On > Behalf Of Harald Tveit Alvestrand > Sent: Thursday, November 17, 2005 1:35 PM > To: Frank Ellermann; ietf@xxxxxxxx > Subject: Re: Diagrams > > 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 > > --On 17. november 2005 17:59 +0100 Frank Ellermann > <nobody@xxxxxxxxxxxxxxxxx> wrote: > > > Steve Crocker wrote: > > > >> 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. > > > > Do you expect Phil's reply before 2007 ? There were some > really nice > > SDL-tools about fifteen years ago. Bye, Frank > > > > > > > > _______________________________________________ > > Ietf mailing list > > Ietf@xxxxxxxx > > https://www1.ietf.org/mailman/listinfo/ietf > > > > > > > > _______________________________________________ Ietf@xxxxxxxx https://www1.ietf.org/mailman/listinfo/ietf