Where does the term witness table come from?

Swift and Haskell both borrow this term from a common source, constructive logic, where proof terms serve as witnesses for their propositions and, in particular, where you prove an existential proposition ∃x:T . P(x) by producing an x which satisfies P and thus serves as a witness to the truth that such an x does indeed exist.

You can think of a protocol requirement as the proposition "there exists a declaration which satisfies this", for which the only possible constructive proof is a witness: a concrete declaration that satisfies it. Value witnesses serve the same purpose for the more basic propositions "values of this type can be copied", "...moved", "...destroyed", etc.; again, the only possible constructive proof is a function which does the operation.

I've been amused over the years by the number of people who assume I just made the term up.

53 Likes