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

[Carsten Bormann <[e-mail]>]

> On 2023-10-27, at 18:32, Marc Petit-Huguenin <[e-mail]> wrote:
> 
> 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.

It is not separating the concepts, but the people being impacted.
For the verification people to do their work, they have to extract a formal description from the specification.  One way to do this is to have the people making the specification use formal description techniques, which may be unfamiliar to them, and cause pushback.  That is all this sentence is about.

> 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."  

(Your term.
I’m more interested in the narrower concept of formal description techniques, which might indeed employ formal languages.)

> 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.' 

… "for the specification, design"…  exactly, that is what a formal description technique is about.

> Formal languages are not formal methods.  

Your term.

> It's like saying that XML is a programming language.  

Non sequitur.

I’m not sure that the rswg is interested in these finer points about formal specification of protocols.

Grüße, Carsten