You say “formal”, which I guess is fine, but I think most people associate “formal” with “everything has a strict all-or-nothing mathematical definition”, whereas I think the data structure would turn out to have everything being fuzzy, like things can range continuously from “100% totally a bookshelf” to “0% absolutely not a bookshelf”, or “a bookshelf in the context of a certain movie where it’s viewed from a particular angle and being used in a particular way, but not in other contexts”, etc. etc. (So the smart contract would have to be something like “if we provide Bird with the following documents and CCTV footage and files, presented in the following order, then Bird will assign >99% truthiness to the statement ‘Party A has tried in good faith to put the strawberry on the plate as further described in the following paragraphs…’”) We can still call that “formal” insofar as there’s a mathematical function that anyone can evaluate on the same data and get the same answer, just as a particular trained ConvNet image classifier can be called a “formally specified” function, i.e. specified by its list of weights and so on. I’m not sure if that’s what you meant.
You say “formal”, which I guess is fine, but I think most people associate “formal” with “everything has a strict all-or-nothing mathematical definition”, whereas I think the data structure would turn out to have everything being fuzzy, like things can range continuously from “100% totally a bookshelf” to “0% absolutely not a bookshelf”, or “a bookshelf in the context of a certain movie where it’s viewed from a particular angle and being used in a particular way, but not in other contexts”, etc. etc. (So the smart contract would have to be something like “if we provide Bird with the following documents and CCTV footage and files, presented in the following order, then Bird will assign >99% truthiness to the statement ‘Party A has tried in good faith to put the strawberry on the plate as further described in the following paragraphs…’”) We can still call that “formal” insofar as there’s a mathematical function that anyone can evaluate on the same data and get the same answer, just as a particular trained ConvNet image classifier can be called a “formally specified” function, i.e. specified by its list of weights and so on. I’m not sure if that’s what you meant.
Yup, that is basically what I meant.