An argument from Jimmy Koppel

Jimmy Koppel has, in various places (see here), advanced pieces of an argument that is significant enough to deserve an independent reference.

Let an interface be a specification of what a given bit of software does (and not, e.g., some abstract class appearing in code).

Premises

1. There is a many-to-many relationship between implementations and interfaces.
2. What the code really is and really does is determined (at least in part) by its interface. In Koppel-ese, code has a logical level.

Conclusions

1. Specifying the behavior of an implementation cannot (entirely) specify what the code really is.
2. Guaranteeing (e.g., through testing) a set of implementation behaviors cannot guarantee that the code is correct.
3. The provable guarantees of the formalization (e.g., through a type system) of an implementation of an object do not ipso facto extend to what the implementation represents. The stock Koppel example helps here: suppose you have an object that returns True iff some internal internal field is at least 65. All the formalism in the world won't distinguish between its being an ASCII alphanumeric-character checker and its being a retirement-age checker, and therefore won't verify that it is a correct implementation of (either) an ASCII character checker or a retirement age checker.

Occasionally useful alternative formulation

All you can test about an implementation is a current, actual set of behaviors. But current, actual sets of behaviors implement many interfaces, in general, because interfaces also include counterfactual behavior (most commonly, behavior under future changes).

And counterfactual difference matters, because code needs to be maintained and should also be semantically correct.

So constraining, verifying, and testing implementations in general fails to constrain, verify, and test it as an implementation of the interface.

Thanks to Robert Beard for helping me clarify this. As always, all mistakes and infelicities are entirely mine.