Comparing design by contract to type systems

Question

I recently read a paper that compared Design-by-Contract to Test-Driven-Development. There seems to be lot of overlap, some redundancy, and a little bit of synergy between the DbC and TDD. For example, there are systems for automatically generating tests based on contracts.

In what way does DbC overlap with modern type system (such as in haskell, or one of those dependently typed languages) and are there points where using both is better than either?

Answer 1

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