No; lookup Calculus of Construction. Dependent types allows you to specify an dependence between different values in your type directly within your type system;

No; lookup Calculus of Construction. Dependent types allows you to specify an dependence between different values in your type directly within your type system; which has great implications for type safety and so on. A classic example is that you can specify the 2-vectors on the unit circle as "{ (x,y) : x,y in R | x^2 + y^2 = 1 }" (read as "the set of real 2-tuples, where their norm is equal to 1".) This is not possible in most languages; the closest you can get in most languages is "{ (x,y) : x,y in R }". My personal pet peeve with dependent types and proof-driven programming in general is the wealth of options in formulating propositions. I've seen at least five different ways of defining equivalency.