It's nice seeing people work with compile-time index types. I've played around with checked array indices using some tricks [0], but checked slice indices obviously require a lot more work.
One application I once thought about is "safe pointers". Suppose we have a bunch of pointers into a buffer, and we want to manipulate them without passing around the original buffer everywhere. The idea would be to use marker types or lifetimes to link the pointers to the original buffer at compile time, so we can use proof values to manipulate them safely.
Of course, the devil's in the details with these sorts of things, so I never got very far. It's great to see an actual implementation of a closely related idea.
It's nice seeing people work with compile-time index types. I've played around with checked array indices using some tricks [0], but checked slice indices obviously require a lot more work.
One application I once thought about is "safe pointers". Suppose we have a bunch of pointers into a buffer, and we want to manipulate them without passing around the original buffer everywhere. The idea would be to use marker types or lifetimes to link the pointers to the original buffer at compile time, so we can use proof values to manipulate them safely.
Of course, the devil's in the details with these sorts of things, so I never got very far. It's great to see an actual implementation of a closely related idea.
[0] https://play.rust-lang.org/?version=stable&mode=debug&editio...