Would be nice to see more exploration of the design space for crates that provide ranged integer types to eliminate bounds checks in Rust. I wouldn't be surprised if you can encode something like Wuffs in Rust's type system.
Conversation
Replying to
It would be interesting to see how usable you could make it. Refinement type systems usually use solvers to avoid some of the tedious proofs you might run into. Aren’t there are number of projects working on taking the latter approach with Rust?
Another limitation might be with monomorphisation. For some use cases you might want to erase the type level ranges at runtime, but rust would instantiate a new impl for each concrete range. Might also make handling dynamically known ranges difficult?
1
1
Still a cool idea though, would be nice to see it explored more!
1