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.
Regards,
Brian