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...

?

On Tuesday, 15 September 2015 at 17:45:45 UTC, Freddy wrote:
> Would it be worth implementing some kind of typestate into the language?
> By typestate I mean a modifiable enum.
>
> [...]

Article about this in C# and F#:

http://enterprisecraftsmanship.com/2015/09/28/c-and-f-approaches-to-illegal-states/