Re: [hackathon] Formal Languages at the Hackathon

From practical experience (as in, implementing and interoping stuff through schema defined packet formats in a performance critical protocol) I think that it is most practical and  long-term productive to concentrate on a format IDL like yang-data or enhance GRPC or thrift with offset/size provisions to model such data. Trying to kow-tow to "human readers" sprinkling stuff full of natural language in ASCII pictures all over the document was a feasible technique when better tools did not exist and complexity was low and people were "reading the wire". Formalizing it further does IMO a long term disservice to IETF @ this point in time for several reasons. 

Having said that, I made exceedingly good experience working on implementation/interop of a whole protocol in Thrift which we chose for its extremely portable open source compiler, maturity, extensive language backend support and rich set of constructs available (maps of even structures to structures, differentiation between a set and a vector and so on). In fact, my view is that you want to train people to NOT look @ packet bits and count offsets to understand what's going on but serialized data is a "blob" on the wire that can be only read after an IDL is applied to decode it. 

As to "reserved", future extensibility and so on we thought through the issues and with versioning of schemas and couple rules this is entirely feasible. At least Thrift parser does reliably differentiate from IDL between optional, optional with default and mandatory fields which is all that is really needed as we verified. 

Schema in protocol spec appendix on https://datatracker.ietf.org/doc/draft-ietf-rift-rift/?include_text=1

BTW, an interesting problem is how we match a packet IDL onto registries. The IANA section you find in RIFT is entirely generated from the schema and IMO that's a viable approach (interesting topic is versioning of schema and how THAT interacts with registries ultimately). Ultimately I believe the IDL should be the source of truth and the registries should just point to schema elements and enforce registry allocation policies, ensure collision-free extension of schema and validate its versioning but not hold codepoints. 

Glad to talk more about it but I'm coming in Sat nite only ... 

--- tony 

On 11/6/19, 7:40 AM, "hackathon on behalf of Carsten Bormann" <hackathon-bounces@ietf.org on behalf of cabo@tzi.org> wrote:

    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://urldefense.com/v3/__https://tools.ietf.org/html/draft-petrov-t2trg-youpi__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNKybg7Y9A$ 

    * 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://urldefense.com/v3/__https://tools.ietf.org/html/draft-ucarion-jddf__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNLGSHOyBg$ 

    * 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://urldefense.com/v3/__https://www.w3.org/TR/wot-thing-description/__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNLJDdphMw$ 
    [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://urldefense.com/v3/__https://www.iab.org/wp-content/IAB-uploads/2016/03/Noise-in-specifications-hurts.pdf__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNIWiw1ecg$ 

    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 <sm@smcquistin.uk> 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://urldefense.com/v3/__https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNL8MUCYaQ$ ,
    > 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://urldefense.com/v3/__https://datatracker.ietf.org/doc/draft-mcquistin-augmented-ascii-diagrams__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNLmRvlHqA$ 
    > Getting started information: https://urldefense.com/v3/__https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNL8MUCYaQ$ 
    > 
    > Thanks,
    > 
    > Stephen
    > 
    > 
    > 
    > _______________________________________________
    > hackathon mailing list
    > hackathon@ietf.org
    > https://urldefense.com/v3/__https://www.ietf.org/mailman/listinfo/hackathon__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNI0zxfnZQ$ 

    _______________________________________________
    hackathon mailing list
    hackathon@ietf.org
    https://urldefense.com/v3/__https://www.ietf.org/mailman/listinfo/hackathon__;!8WoA6RjC81c!SS9exXxoGkZM7iVEI5DC4DeL4o9i0EFxrnC0_t-gygfI7XbeEs4uMNI0zxfnZQ$ 