Does the AGPL Work?

I don't think this works as a loophole in the case where the proxy serves no purpose other than to remove license notices. It might work in a case where the proxy was something transformative, had some other purpose, and failed to preserve licenses in a more passive way.

The key thing to know is that the US legal system runs on counterfactual court cases, and the ideology that informs judges' decisions is not a mechanistic programmer-ideology. In particular, they don't like to rule in favor of things that look like overt gamesmanship. So, when there's flexibility in the interpretation of terms, courts not only can choose interpretations that support the intent of the contract, they will systematically bias their interpretations in that direction. The details of the contract constrain what rulings they have available to choose from, but they usually constrain it less than you think.

If the offer doesn't get displayed to the user, the modified version doesn't offer it.

I've long been sceptical of the Affero-style licence terms.  It certainly DOES work in the sense that it (and GPL3 which makes use of it) is a forbidden license in many companies.  It probably does not work in the sense of letting the software be broadly used and forcing change/wrapper source to be published.

Fundamentally, I'm opposed for copyright to be applied to usage limits, as opposed to distribution limits.  It's fine to prohibit distribution of derivative works without source.  It's annoying (probably legal, but I prefer to just not try) to prohibit USE of code that you legitimately acquired and then privately modified.  I think it's fundamentally non-free software if I'm disallowed from using a modification for my own purposes (even if those purposes are accessible by others).

I know of zero court cases or even successful threats of such, which hinge on this clause.  Companies who are careful just avoid it, companies who aren't ignore it (and either aren't caught or the copyright owner realizes it's not worth pursuing).  Note that simple compilation or repackaging is a modification, so would trigger this, just as distributing a compiled or repackaged version does.

The fundamental tradeoff of getting your software/library to be popular and well used versus limiting the ways your customers can extend and use your software in less-publically-visible ways has changed in the last 30 years.  I think RMSs original goals (no printers you can't hack and recompile) have failed, even while the related concepts (high-quality software that you can adapt to your needs, even if you don't get the pre-adapted code to all your stuff) has become absolutely universal.  I also think that's a great thing. 

Huh, the AGPL doesn't work like my memory of the GPL here.

If it did, then I think the answer would be roughly: you don't need to proactively offer the source, you just need to make it available if someone asks. It would be fine to mail them a USB stick containing the code (though I'm not sure if you'd be able to charge for it).

So when Mastodon has a link to get the code, that's nice but it's not strictly required; and if someone removes that link, you still need to give the source to anyone who asks.

... But the AGPL says you have to "prominently" offer the code, through a network no less. That's not what I expected, and indeed I don't know how it would play out in the scenarios you describe, and mostly wouldn't want to guess.