You can go even further with this in other languages, with things like dependent typing - which can assert (among other interesting properties) that, for example, something like get_elem_at_index(array, index) cannot ever have index outside the bounds of the array, but checked statically at compilation time - and this is the key, without knowing a priori what the length of array is. "In Idris, a length-indexed vector…
Rust has some libraries that can do dependent typing too, based on macros. For example: https://youtube.com/watch?v=JtYyhXs4t6w Which refers to https://docs.rs/anodized/latest/anodized/
Dependent typing requires:
- Generic types that can take runtime values as parameters, e.g. [u8; user_input]
- Functions where the type of one parameter depends on the runtime value of another parameter, e.g. fn f(len: usize, data: [u8; len])
- Structs/tuples where the type of one field depends on the runtime value of another field, e.g. struct Vec { len: usize, data: [u8; self.len] }