Re: Certified C compilers for safety-critical embedded systems

[Aatu Koskensilta <aatu.koskensilta@xortec.fi>]

Alexandre E. Kopilovitch wrote:
> Aatu Koskensilta wrote:
> 
>>Then the impossibility follows from some constraints imposed by these 
>>"reality" requirements, whatever they are, and not from G�del's theorem 
> 
> 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?

 > 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. G�del's 
theorem - again, the Halting Problem seems much more appropriate here - 
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. Otherwise, since G�del's 
theorem says nothing about the intricacies of compiler technology, it's 
simply irrelevant.

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

>>It isn't. There's a very clear sense in which the above claim can be 
>>taken to be about recursive functions - in which case all sorts of 
>>considerations about hard relaity are obviously irrelevant -, in this 
>>case about recursive functions that perform transformations on strings. 
> 
> 
> 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. Otherwise 
Halting Problem tells you nothing about the situation.

>>In hard reality there are very few correct compilers if any, but this 
>>has nothing to do with G�del's theorem or its proof.
> 
> Perhaps you consider G�del's theorem as a property of logicians, which is
> licensed (with some strict conditions) to computer scientists... If so, I must
> disappoint you - not all people agree with that position -:)

I have no such opinions.

-- 
Aatu Koskensilta (aatu.koskensilta@xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus