[curryhoward]

Type signatures can completely encode specifications in systems with dependent types. Of course no mainstream programming language supports dependent types, but it's worth pointing out that in principle a type can encode any property checked by a unit test. Actually, dependent types are strictly more powerful, since you can prove undecidable properties which can't be checked by unit tests (e.g., that a function does the right thing for all possible inputs).