Types are not proofs, but typing derivations are. This is definitely true, thanks for the correction. I have never heard anyone say that types cannot feature

Types are not proofs, but typing derivations are. This is definitely true, thanks for the correction. 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. I agree this is dependent on how you construct blame. In the sense I was talking about, it would be difficult to construct a type system which blamed in the same way -- the type system would essentially require a runtime checker for independent pieces of the program crossing the contract boundary, which I have seen constructions of, but is generally not seen as standard. For background, my contract work was in Racket, so I am of the Scheme school :)