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 ty

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