[hackathon] Formal Languages at the Hackathon

Stephen McQuistin <sm@smcquistin.uk> Wed, 06 November 2019 10:09 UTC

Return-Path: <sm@smcquistin.uk>
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 9D23F12081C for <hackathon@ietfa.amsl.com>; Wed, 6 Nov 2019 02:09:40 -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 (2048-bit key) header.d=smcquistin-uk.20150623.gappssmtp.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 g_wuawe3vLS8 for <hackathon@ietfa.amsl.com>; Wed, 6 Nov 2019 02:09:38 -0800 (PST)
Received: from mail-wm1-x343.google.com (mail-wm1-x343.google.com [IPv6:2a00:1450:4864:20::343]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id 49640120802 for <hackathon@ietf.org>; Wed, 6 Nov 2019 02:09:38 -0800 (PST)
Received: by mail-wm1-x343.google.com with SMTP id t26so2613250wmi.4 for <hackathon@ietf.org>; Wed, 06 Nov 2019 02:09:38 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=smcquistin-uk.20150623.gappssmtp.com; s=20150623; h=from:mime-version:subject:message-id:date:cc:to; bh=+v2kkUUuLEIh+O3mslPmiP2hUy81ufHo3bn8PRl317M=; b=jwmfDyZVgsnyzPizIJtEBxy9N3mz/gduCv0+dFLyKo8tL403mDB57ekB+Mhc1sAlg3 ZRopFsySsombPpXAQzZgMB/bhyKQC/iHAbTOXm07CuDWi4AlsUfCRuffG1R2fek5viy1 gEgEneBz3cE2pFMbkXhGp9bv4D40xuFNxiBh7ec3mS7p/OynHgdNA4zKiRf9c/vCUUZE PDqEaLKCrF0ZNfo5quZLQA8fiXvT8PEMOsV2h5wbORl3f1H9lq0DNNjYa9Pba4wde/Tr /eY1Jjy9Fj9JpqlAeLmEPvbVzsFDNBVeTO+3xcN6mrZSHy2uuu6KTITiDhY6CVH17v1m TWIQ==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:mime-version:subject:message-id:date:cc:to; bh=+v2kkUUuLEIh+O3mslPmiP2hUy81ufHo3bn8PRl317M=; b=Q6PTKSFMykc8U0Dec7Y3EY5LtNmclK46mtUsFA7nJHdGsSMvvM1mnsTKMD5LNI3Z3n QAshceUhcpaZ6p3VXVBhKXlF7SoX607B/y2o1hxRcK7Q2R2RdLjbhWZoDLBDpwCKJb3v PJdzOJ/Pd3nHtLS0aw9m56Jf8STl0cy3zYebzRV6r2mjn49lvbkncmCeA0BI3574ZytC pXPNCN+YbFpO39yTr+s2uGbFgrVM7jKJQKouYAWZMaqttOchmrPM0RoFxvUz0mC+jj4E ZDEzMyWL3X0dirPSnfXbTkhI2RJ0o/ou/cJk/FbDRBC02abWfRFWNLP0lmzZy6zDSw/7 EqAw==
X-Gm-Message-State: APjAAAXKfteKPlZ5JKa0ZShaOuHYnRlcnQy6VoixGZW9Ns0aEauX0abh ubdzchSVRSqhAP83fy/mWdMCmYNoHCI=
X-Google-Smtp-Source: APXvYqwXTleBeAyF/tnXyBUARhoSNDFTWcWJ/BFc5WD4CwWFGI0F1dZnC4j1ttEaTPC1S20mNy0UHA==
X-Received: by 2002:a7b:c08f:: with SMTP id r15mr1622698wmh.45.1573034975637; Wed, 06 Nov 2019 02:09:35 -0800 (PST)
Received: from ?IPv6:2a01:4c8:141c:eec2:b115:60f7:9226:7165? ([2a01:4c8:141c:eec2:b115:60f7:9226:7165]) by smtp.gmail.com with ESMTPSA id m25sm2270544wmi.46.2019.11.06.02.09.34 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 06 Nov 2019 02:09:35 -0800 (PST)
From: Stephen McQuistin <sm@smcquistin.uk>
Content-Type: multipart/alternative; boundary="Apple-Mail=_541E54D3-57B8-4467-A49A-4E4F7CA4D695"
Mime-Version: 1.0 (Mac OS X Mail 13.0 \(3594.4.19\))
Message-Id: <4BD0608C-A277-4130-B85C-D7A75FAEFD8F@smcquistin.uk>
Date: Wed, 6 Nov 2019 10:09:33 +0000
Cc: Colin Perkins <csp@csperkins.org>, Marc Petit-Huguenin <marc@petit-huguenin.org>
To: hackathon@ietf.org
X-Mailer: Apple Mail (2.3594.4.19)
Archived-At: <https://mailarchive.ietf.org/arch/msg/hackathon/SCgjKMYw3r5AxES54T9YdZ-t-tc>
Subject: [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 10:09:41 -0000

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