Re: [hackathon] Formal Languages at the Hackathon

[Marc Petit-Huguenin <[e-mail]>]

Hello,

Thanks Stephen for the introduction to the formal languages projects at the hackathon.

The Augmented Packet Header Diagrams project and the Computerate Specifying project complement each other.  As Stephen said, the former aims at structuring a document so information can be extracted from it.  The latter aims at generating documents that are correct by construction.

The idea of Computerate Specifying was born out of the frustration of having examples in RFCs that do not match the normative text, but evolved since as a generic framework to verify various properties about the data layout and protocol described by an RFC.  This is done by combining in a single file a document formatting language and a programming language with dependent and linear types.

Our goal at the hackathon is to learn more about the applicability of that technique by converting existing I-Ds so examples are correct by construction, and to improve the tooling used to process these modified I-Ds.

So bring your I-D and join us to rewrite it as a computerate specification that contains examples that are correct by construction, and help us improve the quality of the tooling.

ID: https://datatracker.ietf.org/doc/draft-petithuguenin-computerate-specifying/
Getting started information:  https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages

Additionally we are planning for an informal side meeting in a bar (place to be announced later) on Thursday 21 at 8pm for discussion on the general topic of Formal Languages at the IETF.

Thanks.

On 11/6/19 2:09 AM, Stephen McQuistin 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 <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 <https://datatracker.ietf.org/doc/draft-mcquistin-augmented-ascii-diagrams>
> Getting started information: https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages <https://trac.ietf.org/trac/ietf/meeting/wiki/106hackathon/formal-languages>
> 
> Thanks,
> 
> Stephen
> 

-- 
Marc Petit-Huguenin
Email: [e-mail]
Blog: https://marc.petit-huguenin.org
Profile: https://www.linkedin.com/in/petithug