Re: [hackathon] Formal Languages at the Hackathon

Kent Watsen <kent+ietf@watsen.net> Wed, 06 November 2019 15:07 UTC

Return-Path: <0100016e414174ee-1592998e-4a19-4aef-b4ab-afaccc2ca26f-000000@amazonses.watsen.net>
X-Original-To: hackathon@ietfa.amsl.com
Delivered-To: hackathon@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id 7B89B1200F9 for <hackathon@ietfa.amsl.com>; Wed, 6 Nov 2019 07:07:23 -0800 (PST)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -1.897
X-Spam-Level:
X-Spam-Status: No, score=-1.897 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, HTML_MESSAGE=0.001, RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, SPF_NONE=0.001] autolearn=ham autolearn_force=no
Authentication-Results: ietfa.amsl.com (amavisd-new); dkim=pass (1024-bit key) header.d=amazonses.com
Received: from mail.ietf.org ([4.31.198.44]) by localhost (ietfa.amsl.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id qoaQw6BJHrIT for <hackathon@ietfa.amsl.com>; Wed, 6 Nov 2019 07:07:20 -0800 (PST)
Received: from a8-64.smtp-out.amazonses.com (a8-64.smtp-out.amazonses.com [54.240.8.64]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-SHA256 (128/128 bits)) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id 8D0FC120128 for <hackathon@ietf.org>; Wed, 6 Nov 2019 07:07:20 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/simple; s=6gbrjpgwjskckoa6a5zn6fwqkn67xbtw; d=amazonses.com; t=1573052839; h=From:Message-Id:Content-Type:Mime-Version:Subject:Date:In-Reply-To:Cc:To:References:Feedback-ID; bh=NAIKH1EwgzsEyuKJyi2gMC22JsdId1kVq4mFuIBedVs=; b=TYMl+j0AlFofblmONSqvMFmDetJ1hGHseI8dB8jaXuUtpRAnQM8YYzNzTqdSE3Xq HdJ4gJqyB/YgQxepGvOS4fBKwKEN4uQvBpmcLD8JMKBq/egZ0a8wGf9AMKnjyjbcM1X UYmheO6/bk7EY1QOZHes18SN1bFNownAGaBU1yH4=
From: Kent Watsen <kent+ietf@watsen.net>
Message-ID: <0100016e414174ee-1592998e-4a19-4aef-b4ab-afaccc2ca26f-000000@email.amazonses.com>
Content-Type: multipart/alternative; boundary="Apple-Mail=_5811BBDC-4F08-4EC1-81F3-199F78545D03"
Mime-Version: 1.0 (Mac OS X Mail 12.4 \(3445.104.11\))
Date: Wed, 6 Nov 2019 15:07:19 +0000
In-Reply-To: <CALGR9oaiE3N1wGc6n6JZsgHc31PkJmSNKvZOvBUP5p47yP=Fsw@mail.gmail.com>
Cc: Stephen McQuistin <sm@smcquistin.uk>, Marc Petit-Huguenin <marc@petit-huguenin.org>, Colin Perkins <csp@csperkins.org>, hackathon@ietf.org
To: Lucas Pardue <lucaspardue.24.7@gmail.com>
References: <4BD0608C-A277-4130-B85C-D7A75FAEFD8F@smcquistin.uk> <CALGR9oaiE3N1wGc6n6JZsgHc31PkJmSNKvZOvBUP5p47yP=Fsw@mail.gmail.com>
X-Mailer: Apple Mail (2.3445.104.11)
X-SES-Outgoing: 2019.11.06-54.240.8.64
Feedback-ID: 1.us-east-1.DKmIRZFhhsBhtmFMNikgwZUWVrODEw9qVcPhqJEI2DA=:AmazonSES
Archived-At: <https://mailarchive.ietf.org/arch/msg/hackathon/gtBnpf3z_0VoMDRlDEUReizQmkQ>
Subject: Re: [hackathon] Formal Languages at the Hackathon
X-BeenThere: hackathon@ietf.org
X-Mailman-Version: 2.1.29
Precedence: list
List-Id: "Discussion regarding past, present, and future IETF hackathons." <hackathon.ietf.org>
List-Unsubscribe: <https://www.ietf.org/mailman/options/hackathon>, <mailto:hackathon-request@ietf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/hackathon/>
List-Post: <mailto:hackathon@ietf.org>
List-Help: <mailto:hackathon-request@ietf.org?subject=help>
List-Subscribe: <https://www.ietf.org/mailman/listinfo/hackathon>, <mailto:hackathon-request@ietf.org?subject=subscribe>
X-List-Received-Date: Wed, 06 Nov 2019 15:07:23 -0000

I posted an I-D back in February on a similar idea.  The draft refers to YANG modules as an example throughout, but the idea applies equally to any structured format.  The draft does not define a "formal language", so much as define steps for a build-time script, to create self-validating submittable xml2rfc documents.  I haven't picked the project up since due to being busy on other things, but I will again if my chair/shepherd effort-level ever spikes again  ;)

	https://tools.ietf.org/html/draft-kwatsen-git-xiax-automation-01 <https://tools.ietf.org/html/draft-kwatsen-git-xiax-automation-01>

Kent


> On Nov 6, 2019, at 6:24 AM, Lucas Pardue <lucaspardue.24.7@gmail.com> wrote:
> 
> Hello,
> 
> The timing of this is quite good because the QUIC WG have recently been debating the pros and cons of the bitmap diagram for describing packets and frames particularly for variable-length fields, see issue #3115 [1].
> 
> Cheers
> Lucas
> 
> [1] https://github.com/quicwg/base-drafts/issues/3115 <https://github.com/quicwg/base-drafts/issues/3115>
> On Wed, Nov 6, 2019 at 10:09 AM Stephen McQuistin <sm@smcquistin.uk <mailto: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://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
> 
> 
> 
> _______________________________________________
> hackathon mailing list
> hackathon@ietf.org <mailto:hackathon@ietf.org>
> https://www.ietf.org/mailman/listinfo/hackathon <https://www.ietf.org/mailman/listinfo/hackathon>
> _______________________________________________
> hackathon mailing list
> hackathon@ietf.org
> https://www.ietf.org/mailman/listinfo/hackathon