This is a good question. Because (due to personal deficit) it would be hard for me to point to many applications written in capability languages, it would be hard for me to point to a real use of rights amplification. I’m not sure which MarkM example you (@crock) are referring to but the fact that the idea has been independently invented at least three times, and keeps appearing in various forms, and continues to get voluminous discussion on cap-talk and elsewhere, to me suggest it warrants some attention.
First there is Morris 1973 http://www.erights.org/history/morris73.pdf . The motivation here is what is usually called abstract data types or encapsulation, used to check for accidental or intentional crossing of abstraction boundaries. In languages like CLU or Martin-Lof type theory the check can be static, but in an open system or one without static type checking it must be done at run time. This seems pretty basic to me, and I don’t know how to get the same effect without rights amplification. That doesn’t mean there isn’t one.
Second there is E, where rights amplification is used for auditors, among other things. Again, it would not have been introduced if a way to avoid it had been known.
Third there is my 1995 writeup which was trying to address the problem of cooperation between mutually suspicious principals, with a solution that’s essentially the same as auditors (if I remember correctly - I haven’t read it since then).
The same mechanism was taken up for record types in late Scheme reports (I see it in the Revised^7 report). I had added this to Scheme 48 a long time ago, so it’s not really independent of the 1995 writeup, but I was not involved in the decision to bring it into the Scheme report, so that means it’s not just me who saw the need.
In general you revert to rights amplification when you’re going to be handed an a priori untrusted capability and want to know if you can trust it in some way, or more generally speaking if some property applies to it. Challenge/response might be another approach, but there may be risk even in invoking the capability in the first place, so maybe you don’t even want to do the challenge.
Another way to say it is that it’s a mark/recapture pattern. I want to pass you a right that I can use but you can’t, so that you can pass it back to me later for me to use. When I pass it I can hide the right inside a capability, protecting it from you; but that’s not the issue. The question is how do I recognize and recover the right when you pass it back the capability back to me. Yes, I probably already have the right, but it is just one of many that I hold (e.g. instances of my abstract data type), and I have to know which one of them has returned back to me through your data flow.
My apologies for lecturing; you probably know all this.
It would be absolutely brilliant to do away with rights amplification. It is a wart. In a closed system, it is not needed. But in an open system, where mutually suspicious principals are passing capabilities to one another, I don’t see another mechanism proposed that is not essentially the same but more awkward (e.g. EQ). I hope there is another way.
Maybe a place to start would be to look at goblins chat and ask how it could be done without rights amplification, maybe in the State model (which I do not know anything about).
(Footnote: I suspect that seal/unseal/sealed? is not the best way to provide this functionality, either because it might be too strong or because it can be awkward to use. But I don’t yet know what’s better.)