On Sun, 17 Jul 2011 09:38:47 +0200 tlaro...@polynum.com wrote: > > Furthermore, I don't know for others, but I prefer correctness over > speed. I mean, if a program is proved to be correct (and very few are), > complex acrobatics from the compiler, namely in the "optimization" area, > able to wreak havoc all the code assumptions, is something I don't buy.
C's design has compromises in favor of speed to correctness (mainly by underspecifying, by leaving more things upto the implementor). So if you really prefer correctness over speed, you should be using Scheme, ML or Haskell etc but not C! But note that for what C is used for, this compromise is fine (IMHO). But this has made its semantics significantly more complex. C doesn't even have a well defined formal semantics (there have been attempts to define denotational semantics for C subsets but never the whole language, and even such a subset specification is significantly larger than, say, Scheme's). Also note that the ISA implementations these days are quite complex (perhaps even more than your typical program). We don't see this complexty because it is all hidden behind a relatively simple ISA. But remember the FOOF bug? Usually the vendor has a long errata list (typically only available on a need to know basis and only under NDA!). And usually they don't formally prove the implementation right; they just run zillions of test vectors! I bet you would be scandalized if you knew what they do :-) > But how can one rely on a binary that is so mangled that the fact > that you do not see it fail when testing does not prove it will > yield a correct result? And, furthermore, that the code is so chewed > that the proofs of correctness on the source level do not guarantee > anything about the correctness of the compiled result? Most all complex programs have bugs. gcc does, clang does, and so does plan9 cc. The difference is in the degree of bugginess. One uses the best tool available for a given job and then learns to work around its problems. The problem with C/C++ optimization is that these languages are quite complex and it is not always easy to figure out the correct equivalent operations under all conditions. Contrast that with Stalin which does whole program optimization of R4RS Scheme programs and does it extremely well (but extremely slowly!). > My gut feeling is that the whole process is going too far, is too > complex to be "maintenable" (to be hold in one hand), and that some > marginal gains in specific cases are obtained by a general ruin if not > of the certainty, at least of some confidence in correctness. I seriously think you will be happier with Scheme!
