A type $T$ is a specification. A term $t$ of type $T$ is an implementation together with a proof of correctness.
Dependent types are more expressive than simple types found in programming languages. Via the propositions-as-types correspondence they allow us to express logical statements which comprise a specification, rather than just "bare" typing information.
For instance, the type
$$\prod_{k : \mathbb{N}} \sum_{m : \mathbb{N}} \mathsf{prime}(m) \times (k < m)$$
can be read in any of the following ways:
- As a proposition: for every natural number $k$ there is a prime $m$ larger than $k$.
- As a type: the type of functions which take as input a number $k$ and output a triple $(m, p, q)$ where $m$ is a number, $p$ is a proof that $m$ is prime, and $q$ is a proof that $k < m$.
- As a specification: implement a function which takes a number and returns a prime larger than it.
Fancier specifications can be expressed just as well. For instance, we can express the specification for a dictionary as a dependent sum (or a record type if it's available)
$$\sum_{D : \mathsf{Type}}
\sum_{K : \mathsf{Type}}
\sum_{V : \mathsf{Type}}
\sum_{\mathsf{empty} : D}
\sum_{\mathsf{add} : K \to V \to D \to D}
\sum_{\mathsf{lookup} : K \to D \to 1 + V}
\cdots
$$
which is read as follows: we need to specify the type of dictionaries $D$, the type of keys $K$, the type of values $V$, the empty dictionary, and the addition and lookup functions. The $\cdots$ would express the required properties of dictionaries, i.e., logical statements governing the behavior of a dictionary.
