A problem with D contracts

[Andrei Alexandrescu]

On 08/01/2010 07:04 AM, bearophile wrote:
> Walter Bright:
>>> /*@ assert (\forall int i; 0<= i&&  i<  n; a[i] != null);
>>
>> This does not make it simpler, it just makes things more
>> complicated by now having two ways to do a foreach.
>
> The point here is to restrict a lot the kind of code and instructions
> you can put inside contracts, so eventually you will have a chance to
> test them automatically.
>
> When you have copied Eiffel to design D contracts you probably have
> seen that in Eiffel you can't put arbitrary code inside contracts
> (the same is true for contract systems in C# and Java, here it's D
> that is designed in the wrong way). This is a limit that was there
> because otherwise it kills the possibility of enforcing them
> statically.

I think D made the right choice here. The space of contracts that can be 
effectively checked during compilation is very small, and the relative 
complexity of the checkers is very high. (Array bounds checking is a 
classic example.) Restricting contracts to make them statically 
checkable with today's technology would essentially push them out of 
existence.

Andrei