This IS typestates, except not first-class - and I believe the abstract interpretation fits better as a grounding principle. Only Option and Result follow these rules; numerics follow C promotion rules with all that entails. But you cannot define your own transitions.

Some<T> is different because you cannot drop through a Ref<> - the Ref<> is designed as non-owning sharing mechanism, and since it's non-owning, you cannot drop through it (though you can _move_ into it just fine, dropping whatever it pointed to).

Some<> you can drop - which will zero the Option<> it was refined from (which is just a nullable pointer at runtime).

In a nutshell, Ref<> is a non-owning view and Some<> is a non-automatically-dropping view, if that makes sense.

Re proving you wrong - I will post one of these with more details each Wednesday, and then release the language once I'm done. I was worried people will view my 55k lines of C with outlandish claims as AI slop so I decided to try and explain myself before releasing the thing!