[zozbot234]

AIUI, practical dependent types are always evaluated at compile time, but the difference with something like C++ generics is that the types can include references to program bindings that relate to runtime values. This means that dependent types can express proofs evaluated at compile time about the runtime properties of a program.