On Mon, Oct 8, 2012 at 7:12 PM, Lorenzo Caminiti <lorcaminiti@gmail.com>wrote:
Because if the primary role of axioms is to state concept's semantics then I'd expect them to be used to enforce concept's semantics (with some type of compile-time checking) instead than using them for some optimization that BTW is going to be compiler-specific. You standardize axioms but how would you standardize the optimization that a compilers will generate based on them? If such optimization cannot be standardized (I don't think it can) and if that is the main reason for axioms, why are axioms standardized?
You don't need to standardize specifically that certain optimizations must be made, but you can standardize what types of optimizations are allowed given the definition of certain axioms (transformation may be a better word here than optimization). To point to something somewhat similar in C++ already, consider NRVO -- the standard explicitly allows for such high-level optimizations that realistically could change the behavior of a program depending on the definition of a type's copy or move, but these optimizations are not actually required to be performed and in practice only some compilers perform them some of the time. Still, overall I think the specification of RVO in the standard has worked fairly well over the years, and I imagine the same would be true of code transformations performed due to the presence of certain axioms. Also, while you often can't verify axioms (they are, after all, axioms), under certain circumstances a smart compiler may be intelligent enough to notice something like provided axioms being contradictory, etc. In that case, even if the code is expected to compile, a given compiler could at least emit a warning (sort of like how some compilers warn if you are doing something that it can detect would result in undefined behavior, but not all, and the code will generally still compile). You don't need to state in the standard exactly what types of code transformations must be performed and when, only which types of transformations are allowed in the presence of certain axiom definitions. In any case weak != 0 so IMO there's some value != 0 in axioms as
"comments that document the concept's semantics and that are checked for syntax errors".
I agree. -- -Matt Calabrese