A further point here: the formal verification techniques required to prove semantic compliance are still a little ways away (at least in terms of our ability to productionise them), but I think we might be able to design these standards in a way which is both:
- forwards-compatible with formal proofs when they do come, and
- in the short-term, compatible with endorsements by particular parties that a resource logic does in fact implement the semantics of a certain standard
A generalised proof type could go a long way here, where simply assuming that a logic implements a standard when it says that it does is equivalent to a trusted delegation proof which anyone can create. All we really need is a way to clearly state semantic properties…
HOWEVER, for now, this is a research problem, and we should do something pragmatic for the devnets.