Implementing typestate

[Ola Fosheim Grøstad via Digitalmars-d]

On Wednesday, 16 September 2015 at 18:41:33 UTC, Ola Fosheim 
Grøstad wrote:
> I don't think this is possible to establish in the general 
> case. Wouldn't this require a full theorem prover? I think the 
> only way for that to work is to fully unroll all loops and hope 
> that a theorem prover can deal with it.

For example:

Object<ready> obj = create();

for ... {
   (Object<lend#> obj, Ref<Object,lend#> r) = obj.borrow();
   queue.push(r);
   dostuff(queue);
}


On the other hand if you have this:

   for i=0..2 {
     (Object<lend#> obj, Ref<Object,lend#> r[i]) = obj.borrow();
     dostuff(r);
   }

then you can unwind it as (hopefully):

   (Object<lend1234> obj, Ref<Object,lend1234> r[0]) = 
obj.borrow();
   (Object<lend4324> obj, Ref<Object,lend4324> r[1]) = 
obj.borrow();
   (Object<lend5133> obj, Ref<Object,lend5133> r[2]) = 
obj.borrow();

   x += somepurefunction(r[0]);
   x += somepurefunction(r[1]);
   x += somepurefunction(r[2]);

   r[0].~this();  // r[0] proven unmodified, type is 
Ref<Object,lend1234>
   r[1].~this();  // r[1] proven to be Ref<Object,lend4324>
   r[2].~this(); // r[2] proven to be Ref<Object,lend5133>
   r.~this();

If the lend IDs always are unique then you sometimes can prove 
that all constructors have a matching destructor...  Or something 
like that...

?