Subject: Re: [T2TRG] [hackathon] Formal Languages at the Hackathon

From: Carsten Bormann <[email-masked]>
Date: Wed, 6 Nov 2019 18:12:37 +0100

On Nov 6, 2019, at 17:52, Antoni Przygienda <prz=[email-masked]> wrote:
> enhance GRPC or thrift

There are several of these integrated modeling language + encoding scheme ecosystems we could latch ourselves up to.  Actually we did that already with ASN.1 a long time ago, and it is interesting what people who have used it for a few decades now think about it (*).

Obviously there are some requirements for data modeling (mostly around handling evolution) that are better served by using a mature FDT approach than by graphical representation of various encoding stages (the “box notation” we love from RFC79x etc.).  

When the encoding dominates your thinking, they get in the way (e.g., look at how HTTP/2 is encoded).  So being able to describe an arbitrary bespoke encoding with an FDT (like Quentin’s work or YOUPI do, within the limits of their expressibility) may be useful in those spaces.

When the complexity of the data being modeled dominates your thinking, you want a solid encoding scheme such as XML or JSON or CBOR (or you can do the latch-up alluded to above).
For standards that are expected to live for a while (“design for decades”), I prefer situations where the encoding scheme has a life of its own, independent of the FDT, so you can swap your FDT if the old one is broken (just as we moved from W3C XSD to Relax-NG for most XML work).  The integrated approaches may have their own advantages, especially in the time-to-market department, while usually wedding you to a specific toolchain (or tool ecosystem, as with ASN.1).

Grüße, Carsten

(*) Especially after you compensate for the inevitable occurrence of Stockholm syndrome.

---

From: Carsten Bormann <[email-masked]>
Date: Wed, 6 Nov 2019 18:16:22 +0100

Interesting discussion at the hackathon mailing list…

BTW, we are thinking about getting together in a corner of the hackathon room with all the people that work on a hackathon project that employs CBOR, so we can have some chatting about cross-pollination and coordination of that side as well.

Grüße, Carsten

> Begin forwarded message:
> 
> From: Carsten Bormann <[email-masked]>
> Subject: Re: [hackathon] Formal Languages at the Hackathon
> Date: November 6, 2019 at 16:40:11 GMT+1
> To: [email-masked]
> Cc: Carsten Bormann <[email-masked]>
> Archived-At: <https://mailarchive.ietf.org/arch/msg/hackathon/Bu-WHQtU-8gZeiX5O16IZ1bFkOw>
> 
> I’m sharing the below with t2trg as it appears to be highly related to some of our current work.
> 
> I’d also like to point out that formal description techniques (FDT) have been used a lot at the IETF and the IRTF:
> 
> * we know very well how to use ABNF (RFC 5234) for our text-based protocols.  We don’t really have a good way to work with multiple layers of ABNF, though; see the difference between RFC 5988 and RFC 8288 for some recent improvements (but the link between the layers is not formal).  ABNF tools exist for both checking ABNF specs and for automatically generating instances (examples).
> 
> * specific areas have had their FDTs, e.g. RFC 4997 for ROHC, YANG for management, etc.  Specifically YANG is increasingly used not only for its original purpose, describing management information bases, but also for data on the wire (yang-data).  YOUPI [1] is an interesting YANG extension for describing arbitrary binary data.
> 
> [1]: https://tools.ietf.org/html/draft-petrov-t2trg-youpi
> 
> * some RFCs were to a large extent machine-generated text (e.g., RFC 7400) or machine-verified (e.g., RFC 8428), based on models in various FDTs.  Some of these are very domain-specific, but we could still be better on sharing tools (and long-term preserving the sources that generated those RFCs).
> 
> * there is a lively discussion about adding (structural) data modeling (a.k.a. “schemas”) to JSON over at the mailing list of the closed JSON WG (e.g., [2]).  While that discussion is ongoing, we already have CDDL (RFC 8610) for structurally modeling CBOR and JSON data.  Maybe one size does not fit all here.  Similar to ABNF, CDDL tools can check specs, verify instances against a spec, extract/generate code snippets from specs, and generate instances/examples from specs.  One next step here is adding links to application semantics.
> 
> [2]: https://tools.ietf.org/html/draft-ucarion-jddf
> 
> * the WISHI activity in T2TRG looks at modeling data shapes, interaction modeling, and potentially adding protocol bindings towards the wire and application semantics towards the application.  Several SDOs are providing interesting study subjects, e.g., W3C WoT with their Thing Description (TD) [3] and the still somewhat stealthy OneDM group with the Simple Definition Format (SDF) [4].  We’ll discuss this on the Friday before the IETF [5] and work on tools for it at the Hackathon (look for “WISHI”).
> 
> [3]: https://www.w3.org/TR/wot-thing-description/
> [4]: https://github.com/one-data-model/language/blob/master/sdf.md
> [5]: https://github.com/t2trg/2019-11-singapore
> (Yes, you can still register.)
> 
> I understand that the “Formal Languages” activity mostly addresses their use in IETF specifications, and I like that angle — there are other uses of formal description techniques that possible have a different set of requirements, which sometimes cause the requirements of spec writers to be forgotten [6].
> 
> [6]: https://www.iab.org/wp-content/IAB-uploads/2016/03/Noise-in-specifications-hurts.pdf
> 
> So I’m really looking forward to the discussions on Friday, November 15th [5] and at the Hackathon.  Getting something going on cross-pollinating and coordinating the various FDT activities at IETF and IRTF might be a good medium term goal.
> 
> Grüße, Carsten
> 
> 
> 
>> On Nov 6, 2019, at 11:09, Stephen McQuistin <[email-masked]> wrote:
>> 
>> Hi all,
>> 
>> Marc Petit-Huguenin and I are championing formal languages projects at the hackathon in Singapore. Broadly, these
>> projects seek to improve the quality of standards by using formal and structured languages in specification documents.
>> These documents can then be parsed by tooling that can, for example, generate parser code or verify properties for the
>> protocol being specified.
>> 
>> There will be two formal languages projects being worked on: Augmented Packet Header Diagrams and Computerate
>> Specifying. Details for both projects are available on the Wiki at https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages,
>> but I'll give a brief outline of the Augmented Packet Header Diagrams project here. I'll let Marc describe his
>> Computerate Specifying project separately.
>> 
>> The Augmented Packet Header Diagram format (draft-mcquistin-augmented-ascii-diagrams) is a consistent packet header
>> diagram format and accompanying structured text constructs that allow for the parsing process of protocol headers to be
>> fully specified. This provides support for the automatic generation of parser code, and for other benefits that follow
>> from being able to use tooling to process packet header diagrams.
>> 
>> Our goal at the hackathon is to improve both the Augmented Packet Header Diagram format itself, by attempting to rewrite
>> existing I-Ds and RFCs using its syntax, and to improve the tooling, and in particular, its Rust parser generator.
>> 
>> Please join us: we are particularly interested in examples of packet header diagrams that might be challenging to write
>> in the format our draft describes, and in how our tooling might fit into existing workflows.
>> 
>> I-D: https://datatracker.ietf.org/doc/draft-mcquistin-augmented-ascii-diagrams
>> Getting started information: https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages
>> 
>> Thanks,
>> 
>> Stephen
>> 
>> 
>> 
>> _______________________________________________
>> hackathon mailing list
>> [email-masked]
>> https://www.ietf.org/mailman/listinfo/hackathon
> 
> _______________________________________________
> hackathon mailing list
> [email-masked]
> https://www.ietf.org/mailman/listinfo/hackathon

---

From: Antoni Przygienda <[email-masked]>
Date: Wed, 6 Nov 2019 17:20:57 +0000

>    When the complexity of the data being modeled dominates your thinking …

Tony’s dogma: “Complexity of any successful technology _always_ goes up with time” 😉 😉

--- tony

---

From: Carsten Bormann <[email-masked]>
Date: Wed, 6 Nov 2019 22:02:23 +0100

> Tony’s dogma: “Complexity of any successful technology _always_ goes up with time” 😉 😉

Indeed, that’s why I talked about “dominates your thinking” (as opposed to “should dominate your thinking”).

An interesting effect of having a great FDT technique is that it becomes much easier to handle complexity.
A follow-on effect is that, as it is so much easier to put in complexity, you do put in more of that.
Which will hurt you sooner than you think (*)…

So I strongly believe that a prerequisite of using FDT successfully is that the formal model of your shiny new RFC should now fit on one slide.  (Which actually works out for RFC 7071 (+)!)

Grüße, Carsten

(*) I still remember when I first read the ASN.1 for GSM MAP.  All 950 pages [IIRC] of it…
(+) https://tools.ietf.org/html/rfc8610#page-61

---

From: Ted Lemon <[email-masked]>
Date: Wed, 6 Nov 2019 22:11:38 +0100

This is getting kind of long for the hackathon mailing list (not that I object to formal languages!).

> On Nov 6, 2019, at 10:02 PM, Carsten Bormann <[email-masked]> wrote:
>

---

From: Marc Petit-Huguenin <[email-masked]>
Date: Wed, 6 Nov 2019 13:13:49 -0800

Maybe we need a new mailing-list to discuss formal languages...

---

From: Antoni Przygienda <[email-masked]>
Date: Wed, 6 Nov 2019 21:15:51 +0000

All correct, except the "fit on one slide" for the whole model is probably working for anything that is not a real world problem __ unless I misunderstood ... 

--- tony 

On 11/6/19, 1:02 PM, "Carsten Bormann" <[email-masked]> wrote:

    

    Grüße, Carsten
    
    (*) I still remember when I first read the ASN.1 for GSM MAP.  All 950 pages [IIRC] of it…
    (+) https://urldefense.com/v3/__https://tools.ietf.org/html/rfc8610*page-61__;Iw!8WoA6RjC81c!TwrWiCR6j8RDlcPfaISIxVV7xjRnaS04YL0LnKZkf3XxaHeXxM53msCyp2QMaA$

---

From: Stephen McQuistin <[email-masked]>
Date: Mon, 18 Nov 2019 15:06:19 +0800

Hi all,

Given the amount of discussion about this, a new mailing list has been created:

	https://www.ietf.org/mailman/listinfo/fdt <https://www.ietf.org/mailman/listinfo/fdt> ([email-masked] <mailto:[email-masked]>)

The list is for the discussion of formal languages, as they pertain to IETF documents. This includes discussion of the requirements of these techniques, and of their adoption within the IETF.

In addition, a reminder that we’re holding an informal side meeting on Thursday at 8pm. This’ll be at The Winery at CHIJMES (Google Maps: https://g.page/thewinerysg <https://g.page/thewinerysg>) — CHIJMES is across the road from the meeting hotel; once there, The Winery is downstairs. If you’re planning to come along, let us know so that we don’t miss anyone.

Thanks,

Stephen

> On 7 Nov 2019, at 05:13, Marc Petit-Huguenin <[email-masked]> wrote:
>