Re: [Rswg] [rfc-i] draft-mcquistin-augmented-ascii-diagrams

[Marc Petit-Huguenin <[e-mail]>]

On 10/27/23 09:09, Carsten Bormann wrote:
> 
> 
>> On 2023-10-27, at 17:19, Marc Petit-Huguenin <[e-mail]> wrote:
>>
>> Signed PGP part
>> On 10/27/23 07:52, Carsten Bormann wrote:
>>> On 2023-10-27, at 16:35, Kyle Rose <[e-mail]> wrote:
>>>>
>>>> Agree with Michael that this should be in the IETF stream if possible. Seems very cool.
>>>
>>> It actually should be in the IRTF stream, under UFMRG.
>>>
>>
>> I was preparing an email in support for draft-mcquistin-augmented-ascii-diagrams when I saw that comment.  What I was going to say in that email was that we do not have an RG or WG to work on formal languages, although we do have an RG for formal methods.  
> 
> A formal description technique (“formal language”) *is* a formal method.
> At least https://www.irtf.org/ufmrg.html uses “formal method” in this way.

No, and the charter even says that "...the use of formal methods may require the use of unfamiliar protocol description languages...", clearly separating the two concepts.

Let's go back to definitions.  [1] says that a formal language is "[a] language with explicit and precise rules for its syntax and semantics."  On the other hand [2] says that '"Formal Methods" refers to mathematically rigorous techniques and tools for the specification, design and verification of software and hardware systems.' 

[1] https://www.oxfordreference.com/display/10.1093/oi/authority.20110803095829121
[2] https://shemesh.larc.nasa.gov/fm/fm-what.html

> 
>> Most formal methods use formal languages, but not all formal languages are used in support of a formal method ("Affirming the consequent" fallacy).  
> 
> Well, since they *are* a formal method, it is not clear they always have to support another formal method.

Formal languages are not formal methods.  It's like saying that XML is a programming language.  It may become one with additional syntax and semantics, but as it is, it is not.

> Of course there are other formal methods (the charter says “including formal verification and analysis”), and these may need an even greater push to be adequately used in IETF standards development.
> 
>> That's the case for ABNF and its variants, the language discussed in the aforementioned draft, and even RFCXML.  The scope of the charter of UFMRG could be extended, but I do not think that's a good idea as it would dilute the the efforts of that RG[1].
> 
> OK, please reread the charter and tell me where I’m wrong.

I did.


-- 
Marc Petit-Huguenin
Email: [e-mail]
Blog: https://marc.petit-huguenin.org
Profile: https://www.linkedin.com/in/petithug