Re: [irtf-discuss] [115attendees] Usable formal methods side meeting at IETF 115

[Toerless Eckert <[e-mail]>]

Colin:

Thanks for the effort. I hope i can be there!

Q1: What is the suggested email list to discuss this topic ? Continue here
    on irtf-discuss ?

P2: I would like to see that what we call "pseudocode" is explicitly
    included in scope of exploration. We have IMHO successfully used it
    RFCs, even if only in individual one-off cases.

    The charter says "formal methods can make specifications easier to validate
    against desired goals  such as correctness". I think this applies to
    pseudocode - except that i am not sure we would know how to build
    automated correctness checkers for them.

    But that does not make them any less preferrable over english text specification. 
    It may just make them less preferrable over formal methods that do support such
    automated correctness checkers. But they may have other downsides. Aka: choices
    may depend on the compromise between the goals.
    
P3: I can understand the "explicit non-goal" statement in the charter from the
    process perspective (don't step on any IETF toe's given how this is
    supposed to be an IRTF effort), but i think it is important to understand,
    that this effort being an IRTF effort does not stop experimentation on live
    IETF drafts with formal methods.

    There is nothing today that stops IETF authors and WGs working on drafts/RFC
    to include any (in)formal language that they feel help the mision of that
    RFC.

    I would therefore like to suggest a charter item like:

    5. encourage and support IETF authors/WGs to engage with this effort when
    experimenting with formal methods in planned or ongoing IETF RFC to mutually
    gain insight in the feasibility of such methods.

Cheers
    Toerless

On Fri, Nov 04, 2022 at 04:42:21PM +0000, Colin Perkins wrote:
> Hi,
> 
> How should we describe and specify protocols?
> 
> How can we ensure that network protocol specifications are consistent and
> correct, and verify that implementations match the specification?
> 
> The IETF community has long used natural language, English, to describe and
> specify its protocols, with occasional use of formal languages and a some
> limited amounts of formal verification. One of the sessions in the Applied
> Networking Research Workshop at IETF 114 [1] started to discuss whether this
> is the right approach, and to what extent formal methods, structured
> specification languages, and natural language processing techniques can help
> describe network protocols.
> 
> Chris Wood and I are organising a side meeting at IETF 115 to continue this
> discussion, and to assess interest in forming a new IRTF research group to
> explore usable formal methods for protocol specification.
> 
> This will takes place on Thursday lunchtime, 10 November, from 11:30-13:00
> UK time in room Richmond 5 of the IETF meeting hotel (the IAB breakout
> room).
> 
> The draft agenda is as follows:
> 
>   - Welcome, Goals, Motivation, Introductions
>       - (15 mins)
>   - Short presentations (45 mins)
>       - “What are Formal Methods and Why Should We Care?”Jonathan Hoyland
>       - “Formal Specification and Specification-Based Testing of QUIC”, Ken
> McMillan
>   - Discussion of proposed charter (20 mins)
>       - See [Google Doc](https://docs.google.com/document/d/1X1aFFXg-LTNcT4cpo3FZ6w1PwHG33Q0RAUUf-R7Kmus/edit#)
>   - Next steps (10 mins)
>       - Does this seem appropriate for an RG?
>       - Are there volunteers to work on this topic?
>       - What, if anything, have we missed?
> 
> if you’re interested in this topic, please review [the draft charter](https://docs.google.com/document/d/1X1aFFXg-LTNcT4cpo3FZ6w1PwHG33Q0RAUUf-R7Kmus/edit#)
> and come along to the side meeting to give your feedback.
> 
> Hope to see you in London!
> 
> Colin
> 
> 
> 
> [1] https://www.youtube.com/watch?v=tCsiB87s-f4
> 
> -- 
> Colin Perkins
> https://csperkins.org/

> -- 
> 115attendees mailing list
> [e-mail]
> https://www.ietf.org/mailman/listinfo/115attendees


-- 
---
[e-mail]