Re: Verified compilers?

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Wed, 07 Mar 2012 19:49:04 +0200, Niklas Holsti wrote:

> On 12-03-07 11:12 , Dmitry A. Kazakov wrote:
> 
>> I was always wondering why people bother to study grammars, LR, LL parsers
>> and other useless stuff.
> 
> Grammars and the notion of parsing (derivations) rigorously define what 
> a given string of characters means, in some formally defined language.

No. A grammar defines some formal language: a set of strings. The meaning
(program language semantics) is defined informally or else by another
language into which these strings are translated.

The grammar defines only syntax. Even that is defined incompletely for most
cases, e.g. X : constant := 10**(10**(10**10)). Though nobody sheds a tear
about it. An attempt to render all errors as syntax errors would reach
nothing but unreadable diagnostics. Semantic error messages are much easier
to understand. So syntax error messages are few and trivial, e.g. "end if
expected." If I needed to recognize the infamous {ab, aabb, aaabbb, ...}
why should I bother about the grammar? I would count a's and b's and
compare two numbers. That is.

Furthermore the merits of formal grammar definitions are debatable, because
the complexity of grammar descriptions usually make it impossible to judge
if a given string do belong to the formal language or not. Normally BNF is
all one needs to define syntax.

> As far as I can see, the only alternative would be to define the meaning 
> of a language by defining a specific interpreter as the standard 
> interpreter, and defining the meaning of a sentence as whatever this 
> interpreter does, when interpreting this sentence.

Rather translation is the only way to formally define the semantics.

>> This is a great example of making a "science" out
>> of nothing and for nothing.
> 
> 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.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de