Thanks for the write-up. I’ll leave some thoughts on the question of the relationship between the resource-abstraction and the object-abstraction for later, but for now I just wanted to note one complexity that I think we’d need to think about in this kind of effort: for different resource objects with potentially different method implementations to be used together in the context of a single “resource machine” in a way which preserves the desired high-level properties, their method implementations must stand in certain relationships to each other, both at a per-resource level and across resources – for example, delta should bind to kind and quantity (per-resource), and commitments and nullifiers of unequal resources should always be unequal (across-resources).
If we allow arbitrary implementations of these methods, the system can be trivially broken: for example, I could create a new resource which intentionally has the same nullifier as a previously created one, and nullify this new resource to prevent the previously created one from being spent. I’m not sure exactly what this would require in terms of type-systems or descriptions to capture precisely, but I think that we’ll need to address this challenge if we want to really capture the resource machine in an OO model.