Re: [abnf-discuss] Target audience for ABNF

[Paul Kyzivat <[e-mail]>]

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 <[e-mail]> 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