Re: [abnf-discuss] Target audience for ABNF

Sean Leonard <dev+ietf@seantek.com> Mon, 20 November 2017 08:37 UTC

Return-Path: <dev+ietf@seantek.com>
X-Original-To: abnf-discuss@ietfa.amsl.com
Delivered-To: abnf-discuss@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id 558931294BD for <abnf-discuss@ietfa.amsl.com>; Mon, 20 Nov 2017 00:37:56 -0800 (PST)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -1.899
X-Spam-Level:
X-Spam-Status: No, score=-1.899 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, URIBL_BLOCKED=0.001] autolearn=ham autolearn_force=no
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 s5zXnIFk0ze2 for <abnf-discuss@ietfa.amsl.com>; Mon, 20 Nov 2017 00:37:54 -0800 (PST)
Received: from smtp-out-1.mxes.net (smtp-out-1.mxes.net [67.222.241.250]) (using TLSv1.2 with cipher AECDH-AES256-SHA (256/256 bits)) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id 81AF8127B60 for <abnf-discuss@ietf.org>; Mon, 20 Nov 2017 00:37:54 -0800 (PST)
Received: from [192.168.123.7] (cpe-76-90-60-238.socal.res.rr.com [76.90.60.238]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by smtp.mxes.net (Postfix) with ESMTPSA id 3B61D275A7 for <abnf-discuss@ietf.org>; Mon, 20 Nov 2017 03:37:52 -0500 (EST)
To: abnf-discuss@ietf.org
References: <97E6D6C0-7010-46D6-8641-670F10A2504C@seantek.com> <3fbd228d-c6cf-be73-c7f2-f6b15979b852@gmail.com> <477FA5E8-FBAA-47D4-98A6-79DBAE4498C7@tzi.org> <7db503ef-3db4-9a72-6d14-001831742600@gmail.com> <62B9A765-E6EE-4C20-9A4E-58ADA9FDE975@seantek.com> <c10a79f2-5e42-fc00-ed5a-4459064b5af4@gmail.com> <6BF6E482-7EAD-4564-B273-44ADC13E7375@tzi.org> <b979026d-cb07-ad36-58ab-1ba82c0e8263@alum.mit.edu> <f370948e-b738-06fd-7d39-82bf068499f4@gmail.com> <c6e9c6df-0b35-a4df-57ef-8c04e9637acf@alum.mit.edu> <4D0B3FB6-988B-4772-B0AB-C6FA22D7E102@tzi.org>
From: Sean Leonard <dev+ietf@seantek.com>
Message-ID: <093d889d-1932-c5f7-c91f-0e13693a63dc@seantek.com>
Date: Mon, 20 Nov 2017 00:35:52 -0800
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101 Thunderbird/52.4.0
MIME-Version: 1.0
In-Reply-To: <4D0B3FB6-988B-4772-B0AB-C6FA22D7E102@tzi.org>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: quoted-printable
Content-Language: en-US
Archived-At: <https://mailarchive.ietf.org/arch/msg/abnf-discuss/PoBO46bHHfXRcEGSNThvk3woiNE>
Subject: Re: [abnf-discuss] Target audience for ABNF
X-BeenThere: abnf-discuss@ietf.org
X-Mailman-Version: 2.1.22
Precedence: list
List-Id: "General discussion about tools, activities and capabilities involving the ABNF meta-language" <abnf-discuss.ietf.org>
List-Unsubscribe: <https://www.ietf.org/mailman/options/abnf-discuss>, <mailto:abnf-discuss-request@ietf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/abnf-discuss/>
List-Post: <mailto:abnf-discuss@ietf.org>
List-Help: <mailto:abnf-discuss-request@ietf.org?subject=help>
List-Subscribe: <https://www.ietf.org/mailman/listinfo/abnf-discuss>, <mailto:abnf-discuss-request@ietf.org?subject=subscribe>
X-List-Received-Date: Mon, 20 Nov 2017 08:37:56 -0000

On 11/19/2017 10:50 PM, Carsten Bormann wrote:
>> On Nov 20, 2017, at 02:13, Paul Kyzivat <pkyzivat@alum.mit.edu> wrote:
>>
>> Dave,
>>
>> On 11/19/17 7:54 PM, Dave Crocker wrote:
>>> On 11/19/2017 4:19 PM, Paul Kyzivat wrote:
>>>> On 11/19/17 4:08 PM, Carsten Bormann wrote:
>>>>>> On Nov 19, 2017, at 19:56, Dave Crocker <dcrocker@gmail.com> wrote:
>>>>>>
>>>>>> Computers are not the target audience for computer languages.  Human readers are.
>>>>> +10k.
>>>> I agree that the human audience is of major importance.
>>>> But mechanical verifiability of ABNF is also important.
>>> I of course do not mean that computers are irrelevant.  However 'verifiability' invokes formal methods and those typically aren't a concern for typical specification efforts.  Machine processing, yes. Mathematical proofs, no.
>>> I gather you are claiming otherwise.  I haven't noticed any history of formal verification for IETF-related specifications, so perhaps you have some pointers?
>>>> Ideally IdNits would verify ABNF in drafts as a matter of course. IIUC doing so has been included as a requirement for the new tooling. Given the current situation what IdNits can potentially do is very limited.
>>> IdNits hardly seems to qualify as 'verification'.  So I'm probably not understanding exactly what problem you are concerned about.  Details?
>> I'm not talking about verifying/proving that the ABNF does what was "intended". I'm willing to grant (for purposes of IETF documents) that verifying the ABNF reflects the *intent* is done by the human review process.
> Right, but tools like abnfgen can help enormously in this task — the reviewer generates a few matching instances and eyeballs whether they look like what was intended.  Validating a few manually generated instances against the ABNF is the other computer-assisted process in validation.
>
>> I'm simply talking about verifying that the ABNF is entirely well formed, that all rulenames have definitions, and that there are no multiple definitions. (Multiple instances of the same rulename on the left of  an "=“.)
> If the YANG people can do validation automatically upon submission, why can’t we?
>
> (That would probably need the XML, with properly marked up [type=“abnf”] artwork elements.  But we could encourage submitting the XML for drafts that cite RFC 5234 normatively.)

Note: reaex (SeanTek's Regular Expression-Based ABNF Extractor) 
<https://tools.ietf.org/tools/table> properly and accurately grabs ABNF 
out of plain text RFCs and Internet-Drafts each and every time. Includes 
automatic comment generation to annotate where in the RFC the ABNF came 
from. Tested on all of the RFCs in the RFC series.*

Sean

*Succeeds when it's actually ABNF. Skips over stuff that is not actually 
ABNF (including ABNF typos). I think a few superseded RFCs had typos and 
they don't count.