This sounds like two questions: "what axioms are for", and "what should Boost.Contract do about them".
I think that sums up the problem quite well.
I think there is some merit in putting axioms into concepts. ... snip
Third, compilers could make use of the declarations in axioms (even if they cannot validate the "correctness" of an axiom). This is more-less how copy elision works. It works under unverifiable assumption that copy constructor does nothing else but creating a copy of the original object and the destructor does nothing else but destroying an object. This assumption does not always hold: for instance you may be doing some logging in the constructor (and be surprised that the logging vanishes), but compilers are nonetheless allowed to do such substitution (which is in fact an elimination of constructor and destructor call). If we had axioms we could specify copy elision as an axiom, say:
* axiom CopyElision( T v ) {* * { T(v); } <=> {} * * }*
And need not define any special rules for copy elision in the standard. (Well, I know it would not work, but you get the idea.)
I think that trying to define the semantics of the language from within the language gets us to shaky ground because we can't say under what circumstances a copy could be elided. But again, we're in an early state of design w.r.t. a proposal for how axioms might actually be used, and I'm not particularly knowledgeable of those details. I can only say with confidence that it's being worked on.
Regarding question "what should Boost.Contract do about axioms", my opinion is that you should only check them against C++ syntax and type safety. That is, if you see this axiom:
*concept BidirectionalIterator<ForwardIterator I> = requires decrement (I i, I j) { axiom { is_valid(––i) <=> is_valid(i––); is_valid(i––) => (i == j => i–– == j); is_valid(i––) => (i == j => (i––, i) == ––j); } ...*
You should check if expressions: *is_valid(––i), **is_valid(i––)*, *i == j*, *i–– == j*, *(i––, i) == ––j *are valid (compilable), and that's it. That is, whoever is defining concept *BidirectionalIterator *must make sure that function *is_valid *is in scope and does something -- not you.
Yes, and you'll never be able to actually do anything programmatically with is_valid. You might also consider using axioms as test cases for unit testing. This is something that was done by a group in Bergen using a metacompiler. http://www.jot.fm/issues/issue_2011_01/article10.pdf The paper should be free. If not, I can email a version (off-list, of course) to anybody that is interested. And I just returned from presenting a paper on testing generic libraries where I discussed a manual approach to the same problem. The paper hasn't been published yet, but I can make a copy available if you are interested. Andrew