jordan_bonecut

I’ll look into this

I’m not quite sure I understand your question. But if x is a vector of things that contain allocations, the compiler will track a plane for them and represent them sparsely as needed be.

I agree with you, if I were asking for a code review. I'm mostly interested in what people think of the language features. A code review in its current state is not interesting, but I believe the site has some ideas that can be food-for-thought

Because good tools are good

It is different because for many cases you may need to prove your assertions. Consider:

fn foo(x: usize) -> NonZero where x != 5 { NonZero::new(x - 5) }

I do not believe this is achievable in Rust.

Correct, every allocation is its own plane. The nice thing about this model is that you don't need to explicitly call out lifetimes. I also believe that lifetimes aren't really a good model of what actually happens in memory. This model is more powerful because it understands relationships between planes in memory, which Rust's model doesn't. This is why it requires mutable borrows to be unique which is oftentimes overly restrictive. For instance this is not valid Rust:

let x = vec![1, 2, 3]; let a = &mut x[0]; let b = &mut x[1]; swap(a, b);

Because Rust doesn't really know the difference between the whole Vec an element within the vec. Therefore it treats any mutation as one that could potentially invalidate anything with the same lifetime and doesn't compile. So I believe the plane model to be strictly better because it allows for this and still prevents the real scary thing:

let x = vec![1, 2]; let a = &mut x[0]; x.push(3); a = a + 1;

For me part of the fun of such a side project is complete control. I’m willing to risk this over starting from something existing, which may be the wrong call!

I considered waiting longer to share more but felt feedback early was better than waiting for more polish. Will focus on this with high priority though, good feedback

If you want to assume that overflow wraps either:

Your hardware does this OR You implement it in software

Overflow is allowed. Overflow behavior is unspecified, like C++

That, sir, is a hot take

A compare and contrast is good feedback, will work on this

Another thing - when a value is moved or dropped the plane’s type changes from T to shape(T). shape(T) contains unspecified data but has the size and alignment of a T. So you couldn’t safely prove that a moved out/dropped shape(T) is a T

This is good feedback. I will chew on this…

What I’ve showcased is definitely not full fledged dependent types. Support is planned via ideal generics but it’s lower on the priority list to nail down