concepts and interfaces

[Reiner Pope]

Manfred Nowak wrote:
> Martin Hinsch wrote
> 
>> The major difference
> 
> I do not see something like axioms in D.
> 
> -manfred
I've found it difficult to actually understand the use of axioms in 
C++0x concepts.  In general, assertions about semantic behaviors such as 
the examples show (Associativity, etc) can't be trivially (ie, through a 
simple type-checker) proven -- rather, it involves some more elaborate 
theorem proving. I haven't heard any hype about involving automated 
theorem proving in C++0x, so I guess checking of this is either:
   - nonexistent; or
   - done at runtime with asserts -- seems highly reminiscent of in and 
out bodies, and invariants.

I can see the possibility of allowing the compiler to transform the code 
based on these axioms, but it would have to be very insightful to really 
do this in the general case. I think built-in axioms like the 
equivalence (in D) of a = a + b; and a += b; have more room for 
exploitation.

As a form of documentation, it could be useful, but I'm not sure to what 
extent it is better than simply:

// must have a*(b*c) == (a*b)*c for all a, b, c

Maybe someone else knows what use axioms serve?

Cheers,

Reiner