Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Evgeny Panasyuk (evgeny.panasyuk_at_[hidden])
Date: 2012-10-07 20:29:20

06.10.2012 17:11, Andrew Sutton wrote:
>> Does compiler have the authority (from formal point of view of C++
>> axioms) to stop compilation with error in such case(of course, if it
>> able to diagnose that)?
> I believe it should, but I do not know the mechanism that it should
> use to diagnose the error.

There are several unpleasant aspects related to this path (giving "stop 
compilation" authority to compiler when axioms do not fit) :

1. Requiring type to always fulfil axioms, means that we can't use types 
which are "partial" to given axiom.
I.e. types which fulfils only axioms only on some subset of values, or 
subset of cases.

2. I can't even imagine how compiler could do verification in general case.
For instance, we have class that represents set in remote database and 
we have associative union operation defined on a such class. How 
compiler should check associative property of such operation?
Obviously, It is impossible to do such check at compile time, objects 
even don't have actual data members, only handles.
OK, even if compiler would have some data, how it would prove any 
property of operations?
It can't even prove that these operations will halt! (halting problem)

3. Hardness of checking leads to situation when some compilers may check 
more cases than others. Even newer versions of same compiler can be 
smarter than predecessor. Does that mean that code which was compiled OK 
on older version of compiler will be broken on new, "smarter" one?

Best Regards,
Evgeny