Re: Verified compilers?

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 12-03-12 11:43 , Dmitry A. Kazakov wrote:
> On Mon, 12 Mar 2012 00:22:06 +0200, Niklas Holsti wrote:
>
>> On 12-03-11 11:47 , Dmitry A. Kazakov wrote:
>>> On Sat, 10 Mar 2012 22:35:09 +0200, Niklas Holsti wrote:
>>>
>>>> On 12-03-10 12:36 , Dmitry A. Kazakov wrote:
>>>>>
>>>>> 1234 is an example of a language (of decimal literal).
>>>>
>>>> Or an example of octal literals, or hexadecimal literals, or telephone
>>>> numbers. The meaning is not intrinsic in the string; it must be defined
>>>> by other means.
>>>
>>> Which only supports my point.
>>
>> What point is that? You have lost me. Or I you.
>
> The point is that "1234" is meaningless. Whatever way you parse that
> string, it is still nothing but a string.

A string is a string, yes. We are talking about ways to define the 
meaning of strings, in various languages.

>> All language-processing programs, compilers and so on, compute with the
>> meanings of strings.
>
> No. They are computing transformations invariant to the meaning.
>
> Consider the source code of a program. You can modify it without knowing
> what it does, while keeping it doing the same thing.

You must be able to prove that the two forms of the program, P and P', 
have the same meaning. Either you have a definition of the meaning of 
the program, from which you show that meaning(P) = meaning(P'), or a set 
of modification (rewriting) rules R that by definition or assumption do 
not change the meaning, and then you show that P can be transformed to 
P' by applying these rules.

IMO grammars (including attribute grammars) are a very practical way 
define either the meaning or the rewriting rules.

> You can translate a C
> program into Ada without understanding it. A compiler does just same. There
> is no dwarf sitting in the box who understands Ada. There is nobody in.
>
>> First, the meaning must be strictly defined;
>> second, it must be practically computable.
>
> No. Programs deal with incomputable meanings most of the time. Real
> numbers, integer numbers, clock, user input are all incomputable.

Nah. Anything a program can do, is by definition computable. A legal 
program source text always has a computable meaning, with one exception: 
non-termination, which is why the meaning of a program is defined as a 
possibly non-terminating computation, not as the end result.

But this is a debate about the "meaning of meaning". The original 
question was whether the research in formal languages and parsing is 
good and useful (my view) or useless (your view). I don't see any hope 
for agreement.

>> A plain grammar does not define meaning, agreed. The meaning is defined
>> by rules attached to the grammar productions.
>
> No. The meanings are attached to the strings.
>
> But what you said is already sufficient to ditch grammars, since you said
> that it is rather the rules which carry the "meaning." Therefore I can take
> whatever algorithm and attach "meaning" to its transitions/states. From
> this point of view your grammars are just an algorithm among others. Why
> specifically grammars? Why the way of programming using grammars should be
> any better than one using tables, or whatever?

Why do all language definitions currently use grammars? Is it just bad 
influence from adacemic screwballs, inertia, and delusion?

Grammars are declarative, attribute grammars almost so, at least much 
more so than "parse tables".

>> But defining meaning by positional notation does not work so well for
>> the numeric literals in Ada. You would have to exclude underscores from
>> the position numbering, and also handle the optional base specification.
>
> And what is the problem to exclude them?

You have to give rules for it, and these rules make the "positional 
notation" definition of the meaning of a numeric literal string much 
more complex. It is easy to do it informally, by saying something like 
"ignore underscores when you count positions", but doing it rigorously 
(mathematically) is more complex.

> I heard of no one who had any
> difficulty in understanding what Ada numeric literals mean.

I am not talking about intuitive understanding, but about the rigorous 
definition of the meaning (which is not really rigorous in the Ada LRM, 
of course, since numeric literals are considered single tokens with 
values described by English sentences).

> You have much worse problems with Ada, e.g.
>
>     <label-1>  : loop ... end loop<label-2>;
>
> where<label-1>  must be equivalent to<label-2>. It is no problem to any
> human reader to understand what does this mean. It is no problem to a
> recursive descent parser. All Ada compilers handle it effortlessly. It is
> only a problem for the *language* you chosen.

What "problem"? A context-free grammar cannot enforce the two labels to 
be equivalent, true. An attribute grammar can, and a Van Wijngaarden 
grammar can. A yacc-generated parser can.

>> What role does the number
>> 137 play in the meaning of the 137th token in the program?
>
> Depends on what that program does. The meaning of a program is specific to
> the domain, none of the compiler's business.

Now you are using "meaning" with a different meaning, as in "what is the 
program used for". Out of scope.

>>> All computers are finite and all programming languages are effectively
>>> finite both in the terms of the source code length and the number of states
>>> compiler programs may have.
>>
>> This argument is one of the last recourses when you have no good answer.
>
> Because this the killer argument.

For what? For denying the usefulness of grammars? Would you really 
define the Ada language by a "manual" that lists all possible Ada 
programs? I guess the 1983 version would allow programs up to a certain 
size, the 1995 version would allow longer and therefore more programs, 
and so on...

> No computer can parse infinite language
> or compute incomputable. If you want to handle such stuff [and you must all
> the time!] you have to map it onto some finite/computable framework and
> deal within the latter.

Exactly. But since our present computers can deal with very large 
numbers and programs indeed, the mathematical and technical methods we 
use for handling programming languages and programs cannot depend on 
this finiteness, but must use methods that apply to numbers and programs 
of unbounded size, but still of constrained form. Grammars are good for 
that, IMO.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .