08.10.2012 21:46, Nevin Liber wrote:
3. Hardness of checking leads to situation when some compilers may check more cases than others. Even newer versions of same compiler can be smarter than predecessor. Does that mean that code which was compiled OK on older version of compiler will be broken on new, "smarter" one?
I'd say yes.
Is this really a different situation than a more aggressive optimizing compiler breaking old code that happened to be dependent on undefined behavior which just happened to work in the past?
Good example. But, even with this example: in case of aggressive optimizing, code is broken at runtime - compiler does not reject it at compile time. If user states something with axioms, which is not true, more aggressive compiler have rights also to break code at runtime, i.e. by substituting something based on axioms knowledge. Real question is about compile-time code rejection. Or more generally, besides of compilers, is it legal(from formal point of view) to state with axioms something that is not true in all cases, even if we understand all side-effects? I inclined that it should be legal - users will take ALL responsibility regarding axioms in ANY CASE (for instance, because it is impossible automatically check them in general case ), compilers MUST not check/complain. Best Regards, Evgeny