Comment by hmry

Very cool and practical, but specs aren't dependent typing. (I actually think specs are probably more useful than dependent types for most people)

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] }