On this topic, I still didn't give up the desire of generating preconditions from axioms and checking them at run-time. N3351 says not to do so because axioms are not constant-correct but given that axioms only alter dummy variables declared within the concepts and not in user code, I don't see why that is a problem (it'd be like allowing preconditions to declare and alter local variables, the state of the user program outside the contract code will still remain unchanged).
Or you could treat axioms more like invariants: check them before and after every [I do not know what]. The difference from contracts is that when you specify a contract you also implicitly say at which point you expect them to be checked. With axioms you just state an "absolute truth" and it is not clear how often it should be checked. Also note this example of axiom that someone here has already brought up: axiom Allocation(size_t n) { malloc(n) <=> realloc(0, n); } If you just create two hidden values p1 and p2: auto p1 = malloc(n); auto p2 = realloc(0, n); If you try to compare the values the will be not equal, but the axiom still holds. The major issue I see so far with generating and checking
preconditions from axioms is that axioms are programmed using "magic" operations like eq, <=>, is_valid, etc that cannot be implemented :(
I think that to you (the concept library author) only token <=> is the magic. Defining function templates eq(), is_valid() and equality_preserving() will be the problem of the users of your library. These functions are particular to STL; not to generic programming. Regards, &rzej