[IlGrigiore]

Clojure spec is contract programming. You write pre and post conditions to ensure at runtime that Pre -> Program -> Post and every time you call a function pre and post conditions need to be checked. Dependent types analyze that relationship at compile time by proving that given the preconditions the function will produce the desired output. Since this is a compile time check you will not have a runtime penalty.