Virtual Formal Languages Side Meeting 15 May 2020

---

Attendees

• Vivian Band
• Carsten Bormann
• Stéphane Bortzmeyer
• Klaus Hartke
• Dirk Kutscher
• Giuliano Losa
• Stephen McQuistin
• Colin Perkins
• Marc Petit-Huguenin
• Maanas Royy
• Ronald Tse

Meeting Recording

Listen to meeting recording (MP3, 45MB)

Slides

Presenter	Title	Audio Timestamp
Stephen McQuistin	Logistics, Agenda, & Introduction	0:00	Download slides
Stephen McQuistin	Parsing Protocol Standards	11:23	Download slides
Marc Petit-Huguenin	Computerate Specifying: An introduction	23:06	Download slides
Ronald Tse	Metanorma	44:05	Download slides
Carsten Bormann	FDT, networking, IETF	56:55	Download slides

Drafts

• draft-mcquistin-augmented-ascii-diagrams
• draft-mcquistin-quic-augmented-diagrams
• draft-petithuguenin-computerate-specifying
• draft-ribose-asciirfc

Resources

• Formal State Machines (fsm) at IETF 68
• Example of errata in RFC because ASCII diagrams are not checked
• The Idris programming language, used by Marc
• The Metanorma system
• Dagstuhl 11042
• CBOR
• RFC 8610: Concise Data Definition Language (CDDL)

Notes/Minutes

• Stephen opened the meeting by setting out the context: there are a number of interesting FDT projects in the IETF, but no group to address broader, overarching questions about their use.
• Attendees introduced themselves.
• Stephen presented his slides on "Parsing Protocol Standards".
  • Broad goal: shift towards a test-driven development style approach to standards development.
  • First aim: develop a tool that allows parsers to be generated automatically from documents.
  • Design principles to guide the development of FDTs for use within documents: most readers are human, authorship tools are diverse, canonical specifications, expressiveness, minimise required change
  • ASCII packet diagrams already specify much of the protocol's syntax
  • Augmented packet header diagrams: consistent diagram format, structured text language - captures everything need to generate parser code, adheres to design principles.
  • Fits within a larger architecture for parsing standards documents and producing code.
  • Question (Dirk): Was the work mainly focused on specifying PDU formats, or also looking at interactions/behaviour?
  • Stephen: No, at the moment focus is on capturing syntax. This is a good basis for other tools and future work that looks at interactions/behaviour.
• Marc presented his slides on "Computerate Specifying: An introduction"
  • Started IETF work in 1998, attended meetings since 2006 (mostly focused on VoIP). Discovered that a lot of the examples in RFCs are incorrect.
  • Shouldn't, in itself, be an issue: but programmers will opt to build code from examples rather than using the English prose specification.
  • Went through five stages of grief: anger (shouldn't have examples in RFC) -> acceptance (let's fix the examples)
  • Started working on this in 2010: first example was RFC 6544, using code to generate the examples -- examples were as correct as the code.
  • Not smooth: lots of back and forth and iteration - changes to spec -> changes to code
  • Started on an approach that integrated the code and text into a single document. Used AsciiDoc, after surveying different options.
  • At the time, integrated with Curry (based on Haskell syntax). Wrote some documents and RFCs using this setup.
  • Wasn't very satisfying: examples were as correct as the code (so if the code was incorrect, the examples were too). Wanted something that allowed the code to be verified.
  • Rewrote the tooling from scratch, built on Metanorma, and using Idris as the programming language -- solved all the problems he wanted to solve.
  • Computerate specifying: a play on literate programming. Literate programming: adding a document on the code; computerate programming: adding code on top of documents
  • Idea is that all formal languages in RFCs are about ensuring that implementations conform to the RFC. Computerate Specifying is on the other side: making sure that the RFC is correct by construction. Don't care about the code, but about the RFC that is generated.
  • Use Idris to define PDUs and state machines; use literate programming to bind the Idris code and document together.
  • Personally believes that computerate specification is important, but need to convince others -- errata analysis.
  • Labelled each erratum, answering the question: could computerate specifying have prevented this erratum?
  • 25% of errata labelled so far. Of those, 70% couldn't have been solved by computerate specifying. 8% had issues with examples, 8% with formulas (i.e., calculation errors), and 14% with languages (e.g., that were syntactically correct, but that could have been fixed by defining them using a meta-language).
  • Many errors with ABNF, packet diagrams, ASN.1; others with C, XML, other diagrams, and TLS.
  • Question (Giuliano): Is there a repository or some place where we can see this work?
  • Marc: currently, there is a draft that explains the approach. I've computerised the ABNF specification; Git repository with this in, all referenced in the draft. On request, can share the source of the computerate specification draft itself.
  • Guiliano: in practice, people will need to write code in Idris?
  • Marc: yes, and that is a problem. Idris isn't the most brain-friendly language. Went through ~15 languages; choice between Agda and Idris in the end. Idris was more programmer friendly. Acknowledge that it is difficult to become fluent in Idris. Planning to write a tutorial on designing protocols using Idris.
• Ronald presented his slides on "Metanorma".
  • AsciiRFC: AsciiDoc syntax for writing RFCs
  • Used on top of Metanorma, which is an open source, open standards project, that seeks to provide a standard document model for SDOs
  • Participates widely in a number of different SDOs (IEC, ISO), including the IETF.
  • Metanorma: stands for meta-standard
  • Like LaTeXm but backed by a standard document model. The standard document model is ISO-36100.
  • Basic usage of Metanorma: AsciiDoc or other source generated into a document model (represented in XML), and from this, generated into different formats.
  • Similar to RFC XML, except that it works with other SDOs that require a more expressive format than the IETF.
  • Command line tool for installing templates, generating documents. Supported on a lot of different platforms.
  • XML format is the canonical format (for archiving, preservation, generation).
  • All the content written in AsciiDoc is fed into the document model, into the correct place. It handles complex tables, images, and footnotes, for example. There are different AsciiDoc blocks, including support for specialised blocks, for particular SDOs.
  • Automates a number of processes: source and cite terminology from termbases, automatically fetch references for supported SDOs, compliance checking with machine readable requirements, model-based standards generation, ..
  • Importantly, support for cross-publishing: IETF document to ITU document, and vice versa, for example. No need to invest time in reformatting.
  • Question (Colin): is this something that is available now for generating RFCs?
  • Ronald: Yes.
  • Marc: Can confirm this -- is used for the Computerate Specifying draft.
• Carsten presented his slides on FDT, networking, IETF
  • Going to talk about a lot of FDTs quite quickly; not much on draft generation.
  • Doing IETF work since 1993, bringing new applications to the Internet. Has run into various FDTs in the process.
  • Worked on XML (and SGML, pre-XML), ASN.1, ROHC-FN, others.
  • Dagstuhl 11042: looked back, found that the improper use of FDTs was on of the factors that helped kill OSI.
  • Important point: can do a lot of things using FDTs, but need to work with the people that we have. In the IETF for instance, a lot of people don't have a CS background. Need to consider that: esoteric languages, for example, should be avoided: needs to be user-friendly.
  • In developing CBOR, became clear that there needed to be a description format: CDDL
  • Thing-to-thing RG (t2trg): looking at ways of integrating data models used by different stakeholders. OneDM activity.
  • Again: mostly about people, much less about the techniques. Need to bring people along, help them use techniques successfully to get work done. Similarly with developers: get them to use FDTs, rather than falling back to English text.
  • JSON replaced most other structured data formats (except for documents, where XML still dominates).
  • Need to specify what you want to interchange. Generic data model: all that can be said using JSON; specific data model: all that can be said using JSON _for this application_.
  • Should data model specifications be in English, or a machine-readable format?
  • JSON: text-based; CBOR: for binary formats. CBOR has many of the same features of JSON's data model, but with (for example), support for byte strings and extension mechanisms.
  • Text-based formats in the IETF are usually described in ABNF.
  • CDDL is an ABNF-like grammar for structured data, based on Bert Greevenbosch's early CDDL proposal, plus ABNF concepts. Active work on extensions.
  • Data formats are evolving interfaces: formalisation might hinder that evolution.
  • OneDM has the notion of multiple syntaxes, in two dimensions: current and next, and loose (anticipating evolution) and strict. Allows, and even assists in, evolution.
  • Easy to fall into the trap of process confabulation: building software that supports what _should_ be happening, rather than what _is_ happening.
  • FDTs enable validation, but also augmentation, annotation, and transformation. Not just specifying syntax, but also layering in semantic information.
  • Want to bring about a fundamental discussion in the IETF about where FDT use is, and how to improve adoption.
• Discussion (from 1:14:15 in audio recording)
  • Stephen: is there a place for an FDT group, to discuss these issues in a more fundamental, abstract way?
  • Carsten: Fundamental work isn't done in working groups: pushed out to the IRTF. Could define a work programme for a research group that could work together with other efforts (like the CDDL work ongoing in the CBOR WG), to build a common understanding of the objectives and the pitfalls and so on that are in this space.
  • Colin: interesting that we have several projects, starting from different directions, that have come to the same sort of space.
  • Dirk: agree with Carsten. It isn't a research question to come up with a data modelling language, or to extend it, but the research question is how to make these techniques usable and acceptable. I'm also thinking that a research group effort would be good for that. We don't know exactly what to do and how to engineer it: that needs experiments, and looking at different approaches -> research.
  • Colin: agree. Interesting that we're all talking about describing protocols. There is a lot of work on verification, and we haven't even gotten that far yet.
  • Marc: I agree that verification is something that is missing in the IETF. SIP is a good example; took 2 years to verifying 4 simple state machines. Personally, a huge proponent of the petrinet technique, which makes state machine verification obvious. Also wanted to add, on the topic of it being about people, that security is a good example. Security is hard, and many people are the IETF don't know how it works, or how to verify it. We trust other people to do that, and we have people that are very good at evaluating what we are doing. A long term goal (5-10 years): have a formalisation directorate that applies formalisation techniques.
  • Colin: I think TLS is a good example of a protocol that has been formally analysed reasonably well.
  • Dirk: if we think that it is a good idea to pursue this in a RG setting, it would also be possible to look into other aspects of formal specification, beyond data models and PDUs. Also possible to look at protocol interactions/behaviours/state machines. These are long term goals: can start with the slightly lower hanging fruit (data models, PDU specifications), and look towards extending beyond this. Start small, but have a bigger vision/ideas - good framing for a RG charter.
  • Stephen: wonder if a RG is the best place to address the social obstacles; RG might make recommendations or explore solutions but get ignored.
  • Carsten: need to look at the areas where people are struggling. For example, those working on YANG are struggling with evolution. They have a number of mechanisms that are close, but they haven't design with a few towards evolution. If the IETF weren't doing things in this space, then a RG wouldn't be useful. But if we can manage to organise the interactions, we can do a lot.
  • Stephen: need to make sure that it engages practically.
  • Dirk: yes, think this would probably be a slightly different type of RG. Wouldn't be concerned so much with doing research presentations with different formal methods ideas, but maybe being more constructive: perhaps producing tools.
  • Colin: there is a lot of flexiility in how RGs are structured, and I think that something that prototypes tools, has usability in its name, is a nice way of thinking about it. There have been a lot of formalisation tools that can do wonderful things, but that are completely unusuable by people that are actually specifying protocols. Work on session types, for example, for modelling protocol interaction. Quite sophisticated, but requires understanding of type theory.
  • Dirk: one line of work of a group like this would be to look at what has been specified so far, and check whether the tooling is useful; to demonstrate applicability. It is too complicated, it won't be used. Need to think about integration (e.g., with Kramdown).
  • Stephen: what are the concrete next steps?
  • Colin: if heading towards a RG, need to identify the right set of people, sketch out the right things for a charter. Need to show that there is enough interest to make progress. Need to sketch out what the group would look like, what it would want to study, and identify a group of people that are willing to work on these things. If we see that there is a group of people that are getting together to work on this, then maybe it makes sense as a RG.
  • Dirk: Etherpad or something more persistent, to start collecting charter ideas?
  • Stephen: will start a Google Doc or similar, for collaboration, and send out a link on the FDT list.
  • Colin: is anyone interested in working on this? A number of attendees indicated that they were.
  • Marc: final point: I don't think that there is one language or technique for every use case. No one technique can solve all the things. Need a way of being able to describe all the things that are needed to solve all of the things.
  • Dirk: identifying what those are is necessary.
  • Colin: non-goal: produce the one formal language to rule them all.
  • Marc: agree; there is no such thing.
  • It was agreed that work on a charter/proposal outline be started, and another meeting scheduled after that.