In the book Type Theory and Functional Programming [Thompson, S 1999] the author explains the relationship between specifications, types and proofs of functions:
The equivalent specifications can be thought of as suggesting different program development methods: using the ∃∀ form, we develop the function and its proof as separate entities, either separately or together, whilst in the ∀∃ form we extract a function from a proof, post hoc.
This analysis of specifications makes it clear that when we seek a program to meet a specification, we look for the first component of a member of an existential type; the second proves that the program meets the constraint part of the specification.
On this same topic, the commenter writes:
Specifications are in a way "more detailed" types. Or, state the other way, types are more basic specifications. Martin-Lof type theory is precisely about fusing the two ideas into one.
My question is: What is the evidence that that types are more basic specifications, and specifications are more detailed types?