Was checking expressions the only reason they were introduced in the first place?
There were more reasons: 1. The axioms have been with concepts since the inception of concepts. Wherever you see concept StrictWeakOrder defined it is accompained by axioms in this or other form. See for instance: http://www.sgi.com/tech/stl/StrictWeakOrdering.html (section "Invariants"). In this sense axioms try to standardize the existing practise (and are somewhat similar to contract-programming invariants 2. They (would) provide a standardised description of certain properties of the code that could be used by tools for code analysis or generation. For instance tools could auto-generate unit tests. Or certain optimizations could be performed based on the knowledge contained in axioms. Regards, &rzej