What is the thought process behind him using the term "witness"? I can tell it is backed by an interesting perspective and I'd like to learn more about that perspective.
At one point, he said this witness "proved" something ... so is this coming from "propositions as types"?
The use of the term "witness" here comes from constructive logic, where proofs of propositions have actual computational content. There "witness" means the same thing as "proof" but is more evocative that the proof is data that can actually be manipulated.
At one point, he said this witness "proved" something ... so is this coming from "propositions as types"?