Comparing design by contract to type systems

The paper Typed Contracts for Functional Programming by Ralf Hinze, Johan Jeuring, and Andres Löh had this handy table that illustrates whereabouts contracts sit in the design spectrum of "checking":

                   |   static checking    |   dynamic checking
-------------------------------------------------------------------
simple properties  | static type checking | dynamic type checking
complex properties | theorem proving      | contract checking

It seems most answers assume that contracts are checked dynamically. Note that in some systems contracts are checked statically. In such systems you can think of contracts as a restricted form of dependent types which can be checked automatically. Contrast this with richer dependent types, which are checked interactively, such as in Coq.

See the "Specification Checking" section on Dana Xu's page for papers on static and hybrid checking (static followed by dynamic) of contracts for Haskell and OCaml. The contract system of Xu includes refinement types and dependent arrows, both of which are dependent types. Early languages with restricted dependent types that are automatically checked include the DML and ATS of Pfenning and Xi. In DML, unlike in Xu's work, the dependent types are restricted so that automatic checking is complete.

The primary differences is that testing is dynamic and incomplete, relying on measurement to give evidence that you have fully validated whatever property you are testing, while types and typechecking is a formal system that guarantees all possible code paths have been validated against whatever property you are stating in types.

Testing for a property can only approach in the limit the level of assurance a type check for the same property provides out of the box. Contracts increase the base line for dynamic checking.