ucan-wg / spec

User Controlled Authorization Network (UCAN) Specification
https://ucan.xyz
Other
197 stars 18 forks source link

Update terminology: Use "witness" instead of "proof" #22

Closed matheus23 closed 2 years ago

matheus23 commented 2 years ago

Something @expede and I have been talking about. We think you'd usually call what today is contained in a UCAN's "proofs" section "witness".

From my intuition (and I'm not sure about it!) a proof is something that can be "right or wrong" on its own. However, witnesses are just witnesses. They can't be right or wrong on their own, but they can be used to prove something.

expede commented 2 years ago

Kind of confusingly, "witnesses" are used for "proof", so we can say that the prf section is "proof by these witnesses".

expede commented 2 years ago

As an intuition:

Alice: "You say unicorns are real? What's your proof?" [request for proof] Bob: "Here's a unicorn 🦄" [witness]

bgins commented 2 years ago

Bob: "Here's a unicorn 🦄" [witness]

Is "witness" a noun or verb here? Is Bob a witness who can provide proof or is the act of providing proof the witness?

expede commented 2 years ago

@bgins Great question!

The witness is the thing that proves the rule, in this case the specific unicorn 🦄 that Bob is pointing at.

A unicorn is a witness to the fact that at least one unicorn exists. 2 is a witness to the existence of even numbers. This comes from constructive mathematics, where proof is done by showing that you can construct an object that matches your predicate statement.

https://en.wikipedia.org/wiki/Witness_(mathematics)

expede commented 2 years ago

The other thing to note in this system, which is relevant to UCAN, is that (by default) you loose the law of the excluded middle. Things are not "true or false". They are "true" if you can provide a witness, or "I dunno, maybe" otherwise. In the same way that I can't prove that there isn't a unicorn in the wild — there might be 🤷‍♀️

(As an aside, when as a child my partner learned that unicorns weren't real, she also applied this to narwhals. She was many years later shocked to discover that sea unicorns are in fact real 😜)

For UCAN, I can't prove that a particular DID can't do something unless it contradicts the capability's semantics (e.g. can't SEND a DNS record). You always might have a capability hidden somewhere that's not shared with me that can act as a witness to a capability.