- The word 'contract' has different meanings depending on which subcommunity you are talking to. For example, the Penn crowd often uses the word 'contract' in relation to refinement typing. The Scheme folks tend to think of the problem in different terms, but I am not convinced there is any substantial or insightful difference between the various definitions. As you seem to be an expert in the subject, I am sure you have read the manifest contracts paper, but I will leave this link here for the others: http://www.cis.upenn.edu/~mgree/papers/popl2010_contracts.pd....
- I have never heard anyone say that types cannot feature blame. I would argue that, for example, Haskell's type checker is quite good at blaming the correct party for a type violation. To argue the opposite you would need a precise definition of blame, and I am aware there are several papers written on this subject. I am sure you could find a definition of blame that excludes static type systems, but I am not sure that definition would be useful.
- Types are not proofs, but typing derivations are. Even if you consider types and contracts to be different, the execution trace serves as a proof of a dynamically checked 'contract' (which is really just a derivation in an operational semantics).