IETF Logo Mail Archive

Re: [abnf-discuss] Target audience for ABNF

Dave Crocker <dcrocker@gmail.com> Mon, 20 November 2017 00:54 UTC

Return-Path: <dcrocker@gmail.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 8CB12124319 for <abnf-discuss@ietfa.amsl.com>; Sun, 19 Nov 2017 16:54:14 -0800 (PST)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -1.999
X-Spam-Level:
X-Spam-Status: No, score=-1.999 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, FREEMAIL_FROM=0.001, RCVD_IN_DNSWL_NONE=-0.0001, SPF_PASS=-0.001, URIBL_BLOCKED=0.001] autolearn=ham autolearn_force=no
Authentication-Results: ietfa.amsl.com (amavisd-new); dkim=pass (2048-bit key) header.d=gmail.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 pORj_bdDICGX for <abnf-discuss@ietfa.amsl.com>; Sun, 19 Nov 2017 16:54:13 -0800 (PST)
Received: from mail-ot0-x235.google.com (mail-ot0-x235.google.com [IPv6:2607:f8b0:4003:c0f::235]) (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 00F23120721 for <abnf-discuss@ietf.org>; Sun, 19 Nov 2017 16:54:12 -0800 (PST)
Received: by mail-ot0-x235.google.com with SMTP id s12so6365865otc.0 for <abnf-discuss@ietf.org>; Sun, 19 Nov 2017 16:54:12 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-language:content-transfer-encoding; bh=7OGS4tBjCyz/4QH5qd0o8Swqfk2KaFQ/OocJ3g9wqnA=; b=o2YcvRClwmTnGsMXKeJRLWzooAwE3jt6GzHeU/qlY/rmK91TsgqEj8HqytWikRxnxr oUQ3r7hNyzVRnPmEa07jF59S12O0DhImfnNlsduysns4K+ZQZWZ/UqLqec483Itvbbfi xDOkQowoK9wvka7cXMXpkqe/OrLjGKfFb8+SNC56KtgMOHKEQ4f1k0XzIY29RMQvmy94 K/315JYm1dmj+oI9VcsGqgtbJdVZ8QbMfv6eM42TU06OG0M8zPIv8XNJrvMvboG/SY/I pjZ+VCuruN3vAbXYaxn9qLOVay4Ue9ls0MMBEPa4cPWsqqVkR0Ca64ThIBqAwOilg7GW NpmA==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:subject:to:references:from:message-id:date :user-agent:mime-version:in-reply-to:content-language :content-transfer-encoding; bh=7OGS4tBjCyz/4QH5qd0o8Swqfk2KaFQ/OocJ3g9wqnA=; b=LqvezOstXfugIJRAR+ZnYWAe1PxF0yW2kjmg5liITtGSPk7MEYouiGSBcFhVuT15/Y 2E+zUBj3rL4AMDVAU6jukuFYI8UtbUKYLPzXhC8rTgHUY1kUq35LCdG/tUYKBhs1cz/G 9G4PA8VqZLPQ3ypxvT3RCg7i4ZZLohpKiOzsTWnWTkl/IQU3RHlmnuH9jc9z0JVrkIo0 /KFADAi6O0X49wjZ+8FNY4nX9/ZzU9W6hzIIGjnkIFOkIo7kV5TtPwpr2mDNOvwjpdtl 8kwXrAzMuVJqsiD052EtL1QkQytpwpKtRf3yhBuxJkMexydgjUwjGngxkVZneQrntbXM 5nAA==
X-Gm-Message-State: AJaThX77WQOTAIIY45COZshctLq00t1nPLt7pCbYKgTdyMw5y41VyNzA QYIpHRtmFbHs71HDMbY4camlrFg1
X-Google-Smtp-Source: AGs4zMb8mj9n2U6pHcVD3zCCMoAFfQTab8dx5Go+gOJoMaHryX8CuKMiENsQ5F+/FuQ4RESm4Id5/Q==
X-Received: by 10.157.9.196 with SMTP id 4mr7110567otz.173.1511139251754; Sun, 19 Nov 2017 16:54:11 -0800 (PST)
Received: from ?IPv6:2602:304:cda0:8800:c4e8:d795:bbab:6d47? ([2602:304:cda0:8800:c4e8:d795:bbab:6d47]) by smtp.gmail.com with ESMTPSA id h7sm4231708oti.76.2017.11.19.16.54.09 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 19 Nov 2017 16:54:10 -0800 (PST)
To: Paul Kyzivat <pkyzivat@alum.mit.edu>, 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>
From: Dave Crocker <dcrocker@gmail.com>
Message-ID: <f370948e-b738-06fd-7d39-82bf068499f4@gmail.com>
Date: Sun, 19 Nov 2017 16:54:08 -0800
User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:52.0) Gecko/20100101 Thunderbird/52.4.0
MIME-Version: 1.0
In-Reply-To: <b979026d-cb07-ad36-58ab-1ba82c0e8263@alum.mit.edu>
Content-Type: text/plain; charset="utf-8"; format="flowed"
Content-Language: en-US
Content-Transfer-Encoding: 8bit
Archived-At: <https://mailarchive.ietf.org/arch/msg/abnf-discuss/5hRH_GB-ZrFVZZkXzyDlYBkXqn8>
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 00:54:14 -0000

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?

d/


-- 
Dave Crocker
Brandenburg InternetWorking
bbiw.net

v2.23.0 | Report a Bug | By Email