Why I chose D over Ada and Eiffel

[Timon Gehr]

On 08/29/2013 09:17 PM, bearophile wrote:
> Piotr Szturmaj:
>
>> These are refinement types (I call them 'views') and I have
>> half-written DIP for this. However, I doubt that it will be accepted.
>
> I'll be quite interested by such DIP. Even if your DIP will be refused,
> it could still produce several useful consequences.


Why not build something rather general?

struct Hour{
     int hour;
     IsTrue[0 <= hour && hour <= 23] proof;
}


@terminating @correct pure nothrow @safe{ // additional attributes
// allow the compiler to erase proofs at run time in a modular fashion
// to maintain efficiency.

     alias IsTrue[bool a] = Prop[a === true];

     // (selection of intrinsic facts about built-in operators)
     IsTrue[a && b] conj[bool a,bool b](IsTrue[a] x, IsTrue[b] y);
     IsTrue[a] projA[bool a,bool b](IsTrue[a && b] ab);
     IsTrue[b] projB[bool a,bool b](IsTrue[a && b] ab);

     IsTrue[a <= c] letrans[int a,int b,int c]
         (IsTrue[a <= b] aleb, IsTrue[b <= c] blec);
}

struct WorkingHour{
     int hour;
     IsTrue[0 <= hour && hour <= 12] proof;

     @correct // meaning does not throw an error or segfault
     Hour toHour()out(r){assert(r.hour==hour);}body{// compile-time check
         return Hour(hour,
             // an explicit proof that the hour is actually in range
             conj(projA(proof),
                  letrans(projB(proof), IsTrue[12 <= 23].init))
         );
     }
     alias toHour this;
}

(Maybe there is a better choice for the syntax.)

The basic idea is to extend the type system slightly such that the 
compiler becomes able to type check proofs talking about program 
behaviour. A flow analysis ensures that proofs are properly updated.

It would then become possible to build arbitrary refinement types:

bool isPrime(int x){ return iota(3,x).all!(a=>!!(x%a)); }

struct Prime{
     int prime;
     IsTrue[isPrime(prime)] proof;
}

Prime seven = Prime(7,IsTrue[isPrime(7)].init); // proof by CTFE

assert(isPrime(x));
auto foo = Prime(x,IsTrue[isPrime(x)].init); // proof by runtime check 
and flow analysis

auto bar = Prime(y,IsTrue[isPrime(y)].init); // error, disabled @this


This could also be used without runtime overhead eg. inside a 
correctness proof for a prime sieve, though this necessitates a slightly 
larger apparatus than presented here.