> On Oct 27, 2017, at 10:00 PM, Brian E Carpenter <brian.e.carpenter@xxxxxxxxx> wrote: > > Marc, > On 28/10/2017 05:41, Marc Petit-Huguenin wrote: >> On 10/27/2017 08:40 AM, Michael Richardson wrote: > ... >>> * facilitating conformance testing, particularly for open source implementations. >> >> If we are going in that direction then I think it about time that the IETF starts using formal methods to verify protocols, so instead of partially checking that a protocol works (which is the best that hackathons or testing can bring to the table), we have a guarantee that they do work. (self-serving too, as I am working since a couple years on yet another markdown language that does exactly that). > Some of us were very badly burned, in one way or another, > by formal conformance tests of OSI implementations the > best part of 30 years ago. So while I fully support Michael > on "facilitating conformance testing" and would even insert > the word "rigorous", I would be very cautious about "formal > methods" (except for things like MIB modules and YANG, where > clearly a formal check is required). > > Interoperability remains, IMHO, much more important than > formal correctness. Implementations can be formally correct > but faulty in practice. > > In any case, I don't think that distinction is relevant to the > ISOC mission, which needs to retain some level of abstraction. Care must be taken that ISOC does not create an unfortunate feedback loop by sponsoring standards development and conformance testing of implementations. Testing should provide feedback into the standards process, but testing should not drive the standards process. Russ