This is the mail archive of the gcc@gcc.gnu.org mailing list for the GCC project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

Re: g++ and aliasing bools


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

Replace Fermat's theorem with Collatz's sequence (aka Hasse's
_algorithm_).  It's even simpler to state than Fermat, but harder to
prove [1].

The only way to get around this fact is to claim that either (1)
reasoning about recursion is generally hard, or (2) proving an
algorithm terminates is generally hard, which gives me a sense of deja
vu ... =)

So, it is definitely true that reasoning about simple algorithms may
be very difficult.  Q.E.D.

[1] based on the fact it is still unproved, while Fermat is not.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]