Struct should be invalid after move

[Stefan Koch]

On Tuesday, 27 November 2018 at 12:03:20 UTC, Sebastiaan Koppe 
wrote:
> On Tuesday, 27 November 2018 at 10:59:03 UTC, Alex wrote:
>> There exist
>>
>> auto val = Handle.init;
>>
>> 1. How do you treat this?
> I have no idea. Logically I would say that - in my case - the 
> val is invalid.
>
>> 2. Why do you don't want to treat the handle after movement 
>> the same way?
> Because the handle refers to an underlying resource, and any 
> access to that resource through that handle is invalid after a 
> move. Much like one doesn't want to call .release() twice on an 
> unique(T) wrapper type.
>
> Sure, I could put in a runtime check, but then I get runtime 
> errors and I rather have compile time errors.

So ... what you want is this:

"Compiler, ensure that there is no possible execution-flow path 
in which this variable is ever set to 0."

We can actually attempt to prove that, using SMT or other logic 
solvers, though it will most likely say that there is set up 
inputs and flow-decisions which will result in the variable set 
to 0, and it can even give you an example.

You can then take that example and remove the invalid case, for 
the input provided.

This is a massive amount of work to get right.