That's correct, Rust does not have this, in principle Pattern Types (a possible future Rust feature) could do this, but you probably wouldn't use them for this

That's correct, Rust does not have this, in principle Pattern Types (a possible future Rust feature) could do this, but you probably wouldn't use them for this purpose. WUFFS can do this, it calls such types "refined" types - and indeed WUFFS can also do: assert n_bits < 12 via "a < b: a < c; c <= b"(c: width) What that's saying is "As the programmer I say on this line n_bits is strictly less than 12, and I claim you can prove that based on knowing the value of width, and here's why" WUFFS doesn't know how to create such a proof, it's in quotes because WUFFS has a list of proofs a human gave it, baked in, and just accepts any of those proofs, after all a human mathematician assured it these are true. But it can check the rest of your assertion given this proof, and if that fails your software doesn't compile. WUFFS requires that it can see why everything you're doing is OK, whether that's indexing into an array (if you write dogs[k] where dogs is an array of 16 dogs, WUFFS needs to be certain that k is strictly in the range from zero to fifteen inclusive, or the program won't compile) or arithmetic (if bits is supposed to be an integer between one and thirty two inclusive then we can't very well do bits = k * 2 can we, because k might be zero) As a result WUFFS gets to be entirely safe. As a side effect (and also with the help of some clever SIMD friendly language design choices) WUFFS gets to go very, very fast. And all for the very affordable price of abandoning generality. The next Doom, Excel, Apache and Linux cannot be written in WUFFS. But the question is why your thumbnail making code, or your file compressor is written in anything else.