Re: Verified compilers?

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

On Wed, 14 Mar 2012 10:36:51 +0200, Niklas Holsti wrote:

> On 12-03-12 11:43 , Dmitry A. Kazakov wrote:
>> On Mon, 12 Mar 2012 00:22:06 +0200, Niklas Holsti wrote:
>>
>>> 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.

Which can be done without knowing this meaning. It is enough to show that
the meaning (whatever it be) is preserved. This is possible by showing that
P and P' traverse same (or equivalent in some defined sense) states.

>> 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.

Irrelevant. The program operates incomputable meanings, that is the point.
It can be done without computing these meanings, which is why computers are
so useful while being so limited.

A meaning is always incomputable by definition. This is where the process
of computing actually stops, when it reaches a state meaning something to
the program's user.

> A legal program source text always has a computable meaning,

Wrong, it is undecidable to determine what a program computes. And what is
the problem with incomputable meanings? Even wrong meanings? Consider this
program:

   Put_Line ("I have just computed that the Earth is flat!");

> 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).

Well, that debate was around your argument that grammars might have some
virtual usefulness of being a meaning carrier. This does not work either.

>>> 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?

Where you saw any? ARM is not written in BNF. The semi-formal definitions
of lexical elements it contains (nobody could ever care to write full BNF
for Unicode characters) do not define the semantics of Ada. To prove your
point you have to rewrite all ARM in BNF.

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

Huh, you should have argued that they are *less* declarative. Being
declarative is not an advantage and a grammar as a set of rules may look
more imperative than a bunch of 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.

That is easy. Remove all underscores first. (Don't tell me that an act of
removing underscores cannot be formalized or automated.)

>> 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).

That meaning simply does not exist. There are language lawyers thinking
about various language aspects. I don't even know if Ada could be
formalized to a more or less decent level of rigor. In any case, grammars
would be only an obstacle in this mammoth task...

>> 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"?

The problem is with the grammar, it does not define this constraint. What
about the constraint that two objects with equivalent names cannot be
declared in the same scope. Show me the production rule.

> An attribute grammar can, and a Van Wijngaarden 
> grammar can.

Great, why does not the ARM define it that way? Either it does not work or
it is impracticable. Any outcome would support my point.

> A yacc-generated parser can.

We were talking about definitions of meanings, not about compiler programs.
If grammars are so great to define the meaning of loop labels in Ada, where
are these definitions?

>>> 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.

?

That is the only meaning of programs I know.

>>>> 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?

For denying any arguments to infinite languages.

> Would you really 
> define the Ada language by a "manual" that lists all possible Ada 
> programs?

And that would not be enough. For each legal Ada program the definition
must provide its equivalent in some machine language and some run-time
environment.

>> 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.

Sorry, but it is either finite or not. Whatever methods you are talking
about are *sufficiently* finite. You cannot compute incomputable, no matter
what.

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