g++ and aliasing bools

[Gabriel Dos Reis]

Daniel Berlin <dan@dberlin.org> writes:

| On 25 Jan 2002, Gabriel Dos Reis wrote:
| 
| > kenner@vlsi1.ultra.nyu.edu (Richard Kenner) writes:
| > 
| > [...]
| > 
| > | I am very much against the idea of defining a change to be "correct" if
| > | it doesn't cause any regression test failures.  You have to be able to make
| > | an argument that a change is correct independently and the regression tests
| > | serve as a debugger of (among other things) that proof.
| > 
| > I completely agree with Kenner and Mark.  Given, current ABIs
| > supported by g++, aliasing detection is a very subtle issue and we
| > should resist from the temptation of not proving that our algorithms
| > are correct;
| Aliasing is very hard to reason about formally, because no matter what you 
| do, you start running into the undecidability issue.
| In fact, in papers on static type determination for C++ (Do a search on 
| researchindex.org), i've yet to see a *single* formal proof of any kind 
| offered that they are correct.

That is where llies the line between writing a paper to talk about
something and do the actual implementations.  For some reasons, papers
have to abstract over some (important) details.  Something you cannot
aford for in *actual* implementations.

[...]

| Mark's claim that if the underlying algorithm is easy, reasoning about it 
| should be, is also not quite right.

A claim I completely agree with.

| Take Fermat's theorem, for instance.

Oh, come on.

Proof by analogy is fraud.  Secondly, Fermat's theorem is *not* an
algorithm -- it is an *existential* (or non-existential) theorem
without any algorithm specification --- there is no remote relation
about the Fermat's theorem and the concrete issue we have at hand.

-- Gaby