I don't really understand this point. When you reason about a particular type, you must be trying to prove something about it -- what is it that you are trying to prove? That seems like a first draft of the "abstract requirements", no?
I don't really understand this point. When you reason about a particular type, you must be trying to prove something about it -- what is it that you are trying to prove? That seems like a first draft of the "abstract requirements", no?