formal language descriptions

[Henry Spencer]

In article <1187 at garth.UUCP> smryan at garth.UUCP (Steven Ryan) writes:
>>Quite true.  As long as we refuse to admit that unreadability is a major
>>problem that greatly reduces the usefulness of formal standards, they will
>>continue to see little use.
>
>The easy retort is that no formal language is readable or accessible. That
>includes production systems, PL/I, C, Algol, or a hexidecimal dump.

Precisely, which is why none of these methods should be used for a document
that one hopes will be widely read.  Even within such languages, however,
there are gradations of familiarity and accessibility, and the techniques
used in formal definitions are right over at the unfamiliar/inaccessible
extreme.

>>                             Even if the authors of a formal definition don't
>>fall into the trap of "lapidary" writing (paring out every non-essential
>>word that might help the reader make sense out of the formalisms -- a style
>>which is endemic in mathematics), the result is seldom something that an
>>uninitiated reader can tackle without help.
>
>What uninitiated reader can tackle C?

I know a number of people who learned C straight from the reference manual,
back in the days when there basically was no alternative.  Please don't
nit-pick; when I say "uninitiated", I'm not talking about an eight-year-old,
but about a reasonably competent programmer.  Such a person can read a
language definition written in English, but most such people aren't
familiar enough with formal-definition methods to answer a question like
"do I have to make sure that function parameters are not aliased?" from
a formal definition without days or even weeks of study.

>I don't know what your mathematic experience is, but I do know the concise
>and formalism in math is not the math. It's just a way to keep people
>honest...

It is also a booby-trap which has been loudly criticized, even by prominent
mathematicians, for making the literature of the field useless to anyone
but narrow specialists.  Concise formalisms are necessary but not sufficient.

>>... the X3J11 drafts, which can be heavy going at times but
>>*can* be understood without formal background.
>
>And misunderstood. Read this group. Read your own postings...

Formal definitions are not at all immune to many kinds of misunderstandings.
The Peano axioms, no, but a real language definition, yes:  it shares the
problems of massive detail and (unless accompanied by detailed explanatory
material) inadequate explanation and cross-referencing.  God may find formal
definitions of programming languages to be clear and simple; humans do not,
at least not without studying them repeatedly and at length.

>>The attitude that "anyone but an illiterate peasant ought to be able to
>>read formal definitions" is part of the problem, not part of the solution.
>
>I'd hate to have an illiterate peasant at a keyboard, although perhaps that why
>Unix smells. An unwillingness to face that this is an intrinsically difficult
>occupation is part of the problem, not part of the solution.

Intrinsically difficult, maybe.  But it is made much worse by people who
write their language definitions to be read by God, not humans.  Such
people do tend to appeal to the intrinsic difficulty of the problem to
excuse their inability, or unwillingness, to make concessions to the
limitations of their readers.  This is precisely the attitude that I was
criticizing.

>Additionally, not everybody need read the formal definition...  A language
>definition should be complete and concise, sitting on a dusty shelf somewhere.
>It is the contract between users and compilers on what is or is not acceptable
>and what it must mean. 

In other words, it is the sort of document that should be readable to the
users and the compiler writers, so they can understand the terms of the
contract without needing a lawyer to (mis)interpret it.

I would, actually, support a style of language definition in which there
was a formal definition accompanied by a *complete* informal exposition
of the definition, which had been carefully checked for consistency with
the formal one so that it could be used as a reference by the hoi-polloi,
and which was understood to be the partner of the formal definition rather
than an unwanted child of it.  (This means, for example, that a discrepancy
between the two is not automatically resolved in favor of the formal one.)
But that is hard work, and the people who do formal definitions usually
can't be bothered making their gleaming creations understandable to the
unwashed masses who have to use them.
-- 
Intel CPUs are not defective,  |     Henry Spencer at U of Toronto Zoology
they just act that way.        | uunet!attcan!utzoo!henry henry at zoo.toronto.edu