Re: Certified C compilers for safety-critical embedded systems

["Alexandre E. Kopilovitch" <aek@VB1162.spb.edu>]

Aatu Koskensilta wrote:

> > GО©╫del's theorem here is not a foundation or cause, but an explanation of
> > a fact from reality, which was observed many times. 
>
> GО©╫del's theorem is an explanation of what fact? That compilers tend not 
> to be correct? How would GО©╫del's theorem explain that fact?

In short words, real compilers are under high stress, imposed on them by rich
and complex languages, which strive to provide a comprehensive set of features
for a programmer (that is, expressive power) and at the same time to satisfy
various requirements like portability, convenience of maintenance, etc. (that
is, one or another kind of generalization/propagation).

Is this stress inevitable? GО©╫del's theorem says: yes, it is inevitable - while
you are stuck to these goals.

> > And
> > that is what I'd like to say: if you don't know enough about _both_ sides
> > of a correspondence, you can't reasonably judge about its adequacy. It does
> > not matter how deep is your knowledge about one side of the correspondence,
> > if you know too little about another side of it - in this case, have too
> > little experience with internals of production-line compilers, and its real
> > usage in sufficient scale.
>
> My knowledge of production-line compilers is not relevant here.

Interesting. So, you believe that your knowledge of one thing is irrelevant to
your ability to make judgements about its relationship to another thing.

> GО©╫del's 
> theorem - again, the Halting Problem seems much more appropriate here - 

Seems to you - ok, but note that here you are on foreign territory, it is
comp.lang.ada newsgroup, not comp.logic; therefore you if want to be understood,
you should provide arguments familiar to native inhabitants. It may be more
convenient for you (for any reason) to think in terms of some particular
model, but this does not mean that others will share your preferences.

> can only be relevant to compilers, if the compilers are thought of as 
> recursive transformations of programs into programs (in, say, assembly 
> language) or somehow map into formal theories.

Dropping the sacred word "recursive" as inappropriate here, I'd like to inform
you that real production-line compilers aren't just transformations of programs
into programs, that is, from one formal text to another formal text.

First, such a compiler gets at least two input streams, and only one of them
is a formal text. Another always present input stream is the stream of
programmer's intentions. Any real compiler, even of moderate quality, tries
to guess those intentions in many cases/points, and takes them into account.

Second, a real compiler produces at least 3 output streams, and again, only
one of them is (more or less) formal text. Two other always present streams
are diagnostic-errors and diagnostic-warnings, and they aren't formal... even
diagnostic-errors isn't.

(And "getting there is just a beginning" -;)

> Is there a reason to speak about GО©╫del's theorem instead of the 
> undecidability of Halting Problem here?

Certainly yes, because the main problems are not in compilers (algorithms),
but in design of languages.

> > Well, people are different, and some things that happen to be very clear for
> > you, sound like absolute nonsense for me - I simply can't get (and don't want
> > to) why those recursive functions appeared here - they seem (for me, of course)
> > much more irrelevant here than my references to reality.
>
> The Halting Problems speaks about recursive functions. In order to make 
> applications of it to a real world situation, you have to be able to see 
> some things in the situation as being recursive functions.

Recursion means stack, and stack is very human thing, it rarely happens in
non human-made reality. Personally, I like priority queues much better -:) .



Alexander Kopilovitch                      aek@vib.usr.pu.ru
Saint-Petersburg
Russia