Implementing typestate

[Ola Fosheim Grøstad via Digitalmars-d]

On Wednesday, 16 September 2015 at 18:01:29 UTC, Marc Schütz 
wrote:
>             typestate(alias owner) {
>                 this.owner := owner; // re-alias operator
>                 this.owner.refcount++;
>             }

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. Either that or painstakingly 
construct a proof manually (Hoare logic).

Like, how can you statically determine if borrowed references  
stuffed into a queue are all released? To do that you must prove 
when the queue is empty for borrowed references from a specific 
object, but it could be interleaved with references to other 
objects.