Re: [abnf-discuss] Target audience for ABNF

Paul Kyzivat <pkyzivat@alum.mit.edu> Mon, 20 November 2017 17:35 UTC

Return-Path: <pkyzivat@alum.mit.edu>
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 8EFC2129577 for <abnf-discuss@ietfa.amsl.com>; Mon, 20 Nov 2017 09:35:37 -0800 (PST)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -4.201
X-Spam-Level:
X-Spam-Status: No, score=-4.201 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, RCVD_IN_DNSWL_MED=-2.3, SPF_PASS=-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 HRc_EOYUF60D for <abnf-discuss@ietfa.amsl.com>; Mon, 20 Nov 2017 09:35:36 -0800 (PST)
Received: from alum-mailsec-scanner-4.mit.edu (alum-mailsec-scanner-4.mit.edu [18.7.68.15]) by ietfa.amsl.com (Postfix) with ESMTP id BFEB4126E7A for <abnf-discuss@ietf.org>; Mon, 20 Nov 2017 09:35:35 -0800 (PST)
X-AuditID: 1207440f-a5bff70000007960-fd-5a1312652f2f
Received: from outgoing-alum.mit.edu (OUTGOING-ALUM.MIT.EDU [18.7.68.33]) (using TLS with cipher DHE-RSA-AES256-SHA (256/256 bits)) (Client did not present a certificate) by alum-mailsec-scanner-4.mit.edu (Symantec Messaging Gateway) with SMTP id 37.BE.31072.562131A5; Mon, 20 Nov 2017 12:35:34 -0500 (EST)
Received: from PaulKyzivatsMBP.localdomain (c-24-62-227-142.hsd1.ma.comcast.net [24.62.227.142]) (authenticated bits=0) (User authenticated as pkyzivat@ALUM.MIT.EDU) by outgoing-alum.mit.edu (8.13.8/8.12.4) with ESMTP id vAKHZVZk030780 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES128-SHA bits=128 verify=NOT); Mon, 20 Nov 2017 12:35:32 -0500
To: Carsten Bormann <cabo@tzi.org>
Cc: Dave Crocker <dcrocker@gmail.com>, 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: Paul Kyzivat <pkyzivat@alum.mit.edu>
Message-ID: <b44a3940-9317-07e8-ba4e-2e6e0d92f800@alum.mit.edu>
Date: Mon, 20 Nov 2017 12:35:30 -0500
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; 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-Language: en-US
Content-Transfer-Encoding: 8bit
X-Brightmail-Tracker: H4sIAAAAAAAAA+NgFprMKsWRmVeSWpSXmKPExsUixO6iqJsmJBxlMOuArMXTQz/YLI5Muctq 0fl7B6MDs8fOWXfZPZYs+cnkMW1RZgBzFJdNSmpOZllqkb5dAlfGwZbXTAXrFCpal91hbWCc KtXFyMkhIWAi8Wj1c/YuRi4OIYEdTBKvOm8ygySEBB4ySWzZ5Q1iCwMVTeg5yghiiwgoSVy4 uIYNxGYWsJFY9B+kHqR5H4vEuq7lLCAJNgEtiTmH/gPZHBy8AvYSz74qgoRZBFQlGo8+AZsj KpAmcWfGQyYQm1dAUOLkzCdgrZwC1hJ/nrcxQ8w3k5i3+SGULS5x68l8JghbXqJ562zmCYwC s5C0z0LSMgtJyywkLQsYWVYxyiXmlObq5iZm5hSnJusWJyfm5aUW6Zro5WaW6KWmlG5ihIQ0 /w7GrvUyhxgFOBiVeHg/8AhFCbEmlhVX5h5ilORgUhLlXfUbKMSXlJ9SmZFYnBFfVJqTWnyI UYKDWUmEVy0KKMebklhZlVqUD5OS5mBREudVX6LuJySQnliSmp2aWpBaBJOV4eBQkuDtEhSO EhIsSk1PrUjLzClBSDNxcIIM5wEaPgOkhre4IDG3ODMdIn+K0Zijp+fGHyaOZzNfNzALseTl 56VKifPGgZQKgJRmlObBTYOlpVeM4kDPCfOeEQCq4gGmNLh5r4BWMQGtcrnAD7KqJBEhJdXA yHdxgfvUIzkd2Wxrpn170D31daPQZc+Gpy6betxzjApa9lRrCD1IexymfFw74P7VyaGvD0/a e4zLRKHk4zsl6fNOX8PO7ldr2CbyWoF7+uYvdQeX3W0u2NK2boY8p6Zw12b1+k2JG/9XuDcb Vi2v/yTgF3jL2+JBgkSO3MpF52y+LJo1N0PkkRJLcUaioRZzUXEiANjumQYmAwAA
Archived-At: <https://mailarchive.ietf.org/arch/msg/abnf-discuss/tjKctdylz-XvSmX1W17h6iSMLHM>
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 17:35:37 -0000

On 11/20/17 1:50 AM, 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.)

Yes, and I gather that is what is being planned for the future. This 
will work ok if the ABNF is complete and self contained. But there are 
large numbers of important RFCs where it isn't, and in a practical sense 
can't be. For instance RFC6665 is an extension to RFC3261. It includes 
the following as a prelude to the ABNF it includes:

    The Augmented BNF [RFC5234] definitions for the various new and
    modified syntax elements follows.  The notation is as used in
    [RFC3261], and any elements not defined in this section are as
    defined in SIP and the documents to which it refers.

The end result of this is that if you attempt to verify the syntax in a 
standalone way all of the referenced rules are undefined.

(This RFC has the additional issue of using '=' to redefine a rule 
defined in RFC3261. This is historic - it is a revision of RFC3265 that 
was defined prior to the addition of '=/' to ABNF.

There are large number of RFCs that use techniques something like this. 
More modern ones use '=/' and sometimes do something like:

	foo = <defined in RFCxxxx>

That construct eliminates the undefined rules, but the verification then 
fails to check lots of other things.

Another issue is that there is ambiguity about the status of the Core 
Rules defined in RFC5234. Can anyone writing an ABNF grammar assume that 
the core rules are predefined for their use? Or must the grammar 
indicate specifically (how?) that it is implicitly including their 
definitions? If they are automatically present, then they are reserved 
rule names, and cannot be defined differently in any ABNF grammar.

These are impediments to thorough verification of ABNF syntax.

	Thanks,
	Paul