The only analogy I can think of is to a "witness" to a logical proposition in mathematics. In this case the witnesses "prove" that the given concrete type imple

The only analogy I can think of is to a "witness" to a logical proposition in mathematics. In this case the witnesses "prove" that the given concrete type implements the given abstract type. If that's the case it's kind of a weird way to put it, though it sort of squares with the witnesses in proof-relevant formulations of logout where you care about the form of a proof and not just what it proves.