Re: [abnf-discuss] Target audience for ABNF

Paul Kyzivat <pkyzivat@alum.mit.edu> Mon, 20 November 2017 01:13 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 0E911120721 for <abnf-discuss@ietfa.amsl.com>; Sun, 19 Nov 2017 17:13:49 -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 8nAUO2Tl0oLj for <abnf-discuss@ietfa.amsl.com>; Sun, 19 Nov 2017 17:13:47 -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 6E45C1201F8 for <abnf-discuss@ietf.org>; Sun, 19 Nov 2017 17:13:47 -0800 (PST)
X-AuditID: 1207440f-a43ff70000007960-64-5a122c48fcd7
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 24.5A.31072.94C221A5; Sun, 19 Nov 2017 20:13:45 -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 vAK1DhwK017688 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES128-SHA bits=128 verify=NOT); Sun, 19 Nov 2017 20:13:44 -0500
To: 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>
From: Paul Kyzivat <pkyzivat@alum.mit.edu>
Message-ID: <c6e9c6df-0b35-a4df-57ef-8c04e9637acf@alum.mit.edu>
Date: Sun, 19 Nov 2017 20:13:42 -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: <f370948e-b738-06fd-7d39-82bf068499f4@gmail.com>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Language: en-US
Content-Transfer-Encoding: 8bit
X-Brightmail-Tracker: H4sIAAAAAAAAA+NgFvrHIsWRmVeSWpSXmKPExsUixO6iqOulIxRl8HIqu8XTQz/YLDp/72B0 YPLYOesuu8eSJT+ZApiiuGxSUnMyy1KL9O0SuDLmzL/AUnCdt2L3jJ1sDYy/uboYOTkkBEwk Js2/xdzFyMUhJLCDSWLL7/esIAkhgYdMEjO2JYHYwkBFE3qOMoLYIgI2ErsmfmSDaLjOLPGw oZ8JJMEmoCUx59B/FhCbV8Be4vCBW+wgNouAqsTx+0vZQGxRgTSJOzMeMkHUCEqcnPkEqJ6D g1PAVuLMlgqQMLOAmcS8zQ+ZIWxxiVtP5jNB2PISzVtnM09g5J+FpHsWkpZZSFpmIWlZwMiy ilEuMac0Vzc3MTOnODVZtzg5MS8vtUjXRC83s0QvNaV0EyMkUPl3MHatlznEKMDBqMTD+4FH KEqINbGsuDL3EKMkB5OSKO/B9fxRQnxJ+SmVGYnFGfFFpTmpxYcYJTiYlUR4LV0Eo4R4UxIr q1KL8mFS0hwsSuK86kvU/YQE0hNLUrNTUwtSi2CyMhwcShK8d7WA9ggWpaanVqRl5pQgpJk4 OEGG8wANZ9UGquEtLkjMLc5Mh8ifYjTm6Om58YeJ49nM1w3MQix5+XmpUuK8ViDjBEBKM0rz 4KbBks0rRnGg54R5fUEG8gATFdy8V0CrmIBWuVzgB1lVkoiQkmpgrEyIjw73PLcx8oLJv3+O E6Lmn2R4ULOJI9Jt8Zk7rLO0AqRZBWPPni5QXm4Y+mmfh2d8+eHnqhdrPB8ybLzBUbg3aCOX 2R/fh7/1Vp2RTgzKvleYdmKy53OOPVdDdl9ZmJ/pGDVz4UqJezX83Cdm8ib+nrQvpyA24mbx 6tlflS7M/fBMfeczXiWW4oxEQy3mouJEAAeLMkARAwAA
Archived-At: <https://mailarchive.ietf.org/arch/msg/abnf-discuss/jf_cxzEU0OJInDZS4aXnknxiLSE>
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 01:13:49 -0000

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.

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 "=".)

	Thanks,
	Paul