Hi Martin, I agree with your points below, if any one finds an error in IETF standards then should report it on this list or write an ID about that to community, AB ++++++++++++++++++++++++++ Sub: Re: A proposal for a scientific approach to this question [was Re: I'm struggling with 2219 language again] http://www.ietf.org/mail-archive/web/ietf/current/msg76710.html >I believe that the problem with the formal logic is that it is difficult to both write as well as read/understand, and to verify that the chosen "axioms" actually reflect (and lead to) the desired behaviour/outcome, the relative of scarcity of suitable tools, the complexity of the underlying theory and tools, and the tools' resulting lack of "intuitive usability". >> Once you have both, there is still the problem that if a bug or ambiguity >> shows up, For any formal proofing system worth its dime, this can be 100% ruled out, since the proofing system will emit a 100% bugfree implementation of the spec in the programming language of your choice as a result/byproduct of the formal proofing process. >> >> neither the code nor the formal spec nor a prose spec can be taken >> be the right one. What is right is still in the heads of the authors. But maybe you're not really thinking of a defect in the implementation (commonly called "bug") but rather a "gap" in the specification that leads to unintended or undesired behaviour of a 100% bug-free implementation of your spec. (see Section 4 of this paper for an example: http://digbib.ubka.uni-karlsruhe.de/volltexte/documents/1827 ) Donald Eastlake wrote: > > Another problem is maintenance. Protocols change. Having to maintain a > formal specification is commonly at least an order of magnitude more > effort than maintaining a prose description. Definitely. Discussing protocols at the level of formal specification language would be quite challenging (typically impossible in an open forum, I believe it is even be difficult in a small and well-trained design team). > > And, as has been mentioned before, I'd like to emphasize that the IETF > experience and principal is that, if you want interoperation, > compliance testing is useless. Ouch. I believe this message is misleading or wrong. Compliance testing is VERY important, rather than useless, Compliance testing would actually be perfectly sufficient iff the spec was formally proven to be free of conflicts and ambiguities among specified protocol elements -- plus a significant effort spent on ensuring there were no "gaps" in the specification. As it turns out, however, a significant amount of implementations will be created by humans interpreting natural language specifications, rather than implemenations created as 100% bug-free by-products of a formal proof tool, and often, interop with such buggy, and often spec-incompliant implementations is desirable and necessary since they make up a significant part of the installed base. > > The way to interoperation is interoperation testing between > implementations and, to a first approximation, the more and the > earlier you do interoperation testing, the better. The #1 reason for interop problems and road-block to evolution of protocols is the wide-spread lack of compliance testing (on the flawed assumption that it is useless) and focus on black-box interop testing of the intersection of two subsets of protocol features. The problem with interop testing is that it really doesn't provide much of a clue, and the results can _not_ be extrapolated to features and areas that were not interop tested (typically the other 90% of the specification, many optional features and most of the extensibility). The near complete breakage of TLS protocol version negotiation is a result of the narrow-minded interop testing in companion with a complete lack of compliance testing. If done right, pure compliance testing can go a long way to providing interop. The only area where real interop testing is necessary is those protocol areas where the spec contains conflicts/inconsistencies that implementors didn't notice or ignored, or where there is a widespread inconsistencies of implementations with the specification, of created by careless premature shipping of a defective implementation and factual creation of an installed base that is too large to ignore. -Martin