Re: Usefulness of Formal Notions in Programming (was: Verified compilers?)

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 07.03.12 21:17, Dmitry A. Kazakov wrote:

>>> This is a great example of making a "science" out
>>> of nothing and for nothing.

Nothing seems inherent in knowing grammars that prevents good use
of this knowledge. Uses in general system design, or in programming,
or in talking about programs, and all these activities need not have
to do with string processing. Granted, for the knowledge to be useful,
the programmer need not have specialized in grammars.

Two examples:

1. Suppose someone knows what a regular language is.

Let a regular language be taught together with finite automata,
Knowing some of the latter can instruct the design of a system whose
structure (processes, their interactions, ...) is easier to understand
because there is, in fact, a state machine that describes it.

Knowing that general regular expressions, of the CS kind, are made
by obeying simple rules will help writing REs of any variety, and
correctly at that. (I'll claim this.)

2. Suppose someone remembers some things about brackets and CFGs.

A system might have a nested structure. Things in the system first
begin and then end by first taking, and then releasing, resources, say.
Later, depending on an instance of I/O at some point, the program will
choose from a alternative nested structures.
When explaining the program's structure to someone knowing a scheme
such as a CFG, the analogy paves the way towards an understanding
of the structure of the system.

The useful relation between grammars and programming in these cases
is this:

If a person knows one simplified, abstract notion well (grammar),
the he or she will more easily understand a different notion, provided
there is an analogy, or correspondence. I'd give a similar argument
for writing programs.

It seems somewhat like knowing math. If you know it, and know how to
put math to good use, it helps understanding programs, and writing
programs,


>> The various types of grammars and the corresponding parsing procedures
>> help us understand which parsing methods work for which kinds of
>> grammars.
>
> Maybe, but they are totally irrelevant for the grammars of real programming
> languages. On one hand these classes do not capture real differences
> between syntaxes of programming languages. On the other hand, the classes
> they do describe have no other practical interest than torturing students
> of CS classes.

Counting, as you suggest for ab, aabb, aaabbb, ... turns out to be a
delusive solution. It is slippery, at least for use in programming
languages' syntaxes.

For example, Lisp interpreters would be counting brackets that match.
((())). When they have found N left brackets, they'd need to find N
right brackets, too.  Or, really, at least N right brackets, a relation
to which the makers of Lisp had submitted. For, if a programmer had
forgotten to write some right bracket in the middle of a program, the
remaining lists would pile up, the remainder of the program's text
would be added to the most recently opened list.  The dreadful
consequence is that the parser will report nothing but a "syntax error
at end of file". An error not easy to spot, and, therefore, not easy
to fix.  You would hope to be helped by a Lisp system or a pretty
printing editor.  Thus, placement and counting of embedded ((()))s
will require extreme care on the part of the programmer.  But! It is
possible to amend the grammar, and it has been done, see below. This
change cannot, however, be performed if we just focus on counting,
I think.

Consequently, reflecting the fact that programmers do not emit from
productions, but make mistakes, Lisp allows any number of right
brackets to be written in certain places to help with () matching.
For example, when closing a DEFUN list.


A less ()y solution is found in some programming languages.
Their grammars use indexed pairs of brackets, such as occur in

  "begin" ... "end"

or

  [�L�:] loop" ... "end loop [�L�]"

or

  "package �L� is" ... "end [�L�]"

Don't know whether or not a van Wijngaarden grammar can produce the
last sentences. The Ada LRM uses natural language statements such as
"a name) at the end of the right bracket must match the index at the
corresponding left bracket."

In any case, I'll bet knowing grammar at all will help one produce(!)
program designs that are easier to understand if a known scheme is
used, as outlined above.

The word marked (!) in the last sentence points out the recursive
nature of the subject. ;-)