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?
What is the evidence that that types are more basic specifications, and specifications are more detailed types?
functional programming
As Gilles points out, it depends on what you count as types. If you mean by types something liketypes in Java or Scala or Haskell, then this is clearly true.One easy way to see this is (simplifying a bit) to use a general framework ofspecifications to express the behavioural content of types as aspecific case of specification. The best framework to do this at themoment is $\pi$-calculus as a programming language and Hennessy-Milnerlogic as a specification language. I suggest to choose $\pi$-calculusbecause it's expressive, and well studied. In particular, mostsequential programming languages are easily seen to be (behaviourallyequivalent to) specific sub-calculi of $\pi$-calculus.  Hennessy-Milnerlogic is an expressive modal logic that can be used to nail downprocesses up to behavioural equivalence.  Now we take an arbitartytype, say the function space constructor$   int \rightarrow bool$and express the constraints this type imposes on programs as aspecification in Hennessy-Milner logic.Conversely, we need to show that specifications are strictly moreexpressive than types but that's fairly obvious, for we cannot specifye.g. that a method is sorting its input array.