The FULU repository went up May 12. The developer took his repository down on April 23rd.
Others went up earlier: https://github.com/dafik/OrcaSlicer-bambulab
Unless some very fast-paced discussions happened behind the scenes, he could have had no idea a replacement would go up when he took his repository down.
Nowadays, when a popular repository goes down, one can be confident someone will upload a backup, even with a weak legal threat
Furthermore, is FULU maintaining the code or just re-hosting the original? Now the developer is out of the way all Bambu needs to do is make a small change to obsolete the backed-up version.
(Although it's not the only possibility and maybe they're wrong) that Bambu didn't make this small change is evidence they expect someone would fix the repository.
I wouldn't want to take that bet. Would you?
Not personally, but the multiple people re-uploading the repository are.
Brainwavez
26d ago
the developer who made a workaround to now-removed functionality immediately took it down without any attempt to fight a legal case
Of course he did, because others already forked it. And if Bambu still tries to sue him, Louis Rossman has pledged to pay his legal fees.
“Continue to function” was the exact phrase on their website. And “perpetual license” maybe not technically, but literally implies it works perpetually.
Moreover, it’s not an online service that would cost Microsoft to continue hosting it. All that’s needed to keep it running is to push a small update that disables the DRM. I’m confident that’s more than doable for Microsoft: even if they lost the original code, they have ChatGPT and Claude to reverse-engineer the software, or when (inevitably) a crack releases, instead of DMCAing they can adopt it themselves.
I think that generally, it’s harder for game companies to successfully even threaten a frivolous lawsuit, than to defend a legitimate one.
The game company’s lawyers can defend the government’s lawsuit, or the hobbyist sued for bypassing EOL-not-EOL software can get enough people and attention on their side to recover any financial damage and Streisand the game company.
The problem with adding regulations is that they may be applied to smaller devs. Removing regulations, so that some smaller devs’ software may be deemed EOL too early, is less of an issue; because smaller devs already have weaker DRM and lawyers, and thus rely on good faith to defend against piracy (which seems to work well enough).
Brainwavez
27d ago
Even permanently requiring the game to be downloadable may be too much for an individual or small company that has gone bankrupt.
But I support, if it works (or should work) offline, not having legal avenues to stop people keeping and playing the old version (including bypassing DRM for their offline copy).
Brainwavez
27d ago
The theorem that specifies that an off switch turns the system off cannot be proven by a proof that specifies that an off switch turns the system on. It's analogous to the theorem that off maps to false, not that Toggle and Bool are isomorphic (which is similar to your original example).
I can prove that Toggle and Bool are isomorphic by defining a function toggleToBool that maps off to true, another that maps true to off, and showing composition both ways is identity. For that theorem specifically, it doesn't matter that toggleToBool is backwards. I cannot prove that toggleToBool off = false, analogous to "the off switch turns the system off", with that definition.
Likewise, if ChatGPT proves the main theorem with backwards definitions, it doesn't matter, like QT-1 in Asimov's short story Reason. If the main theorem is "the off switch turns the system off" and ChatGPT programmed the off switch to turn the system on, it will simply fail to prove.
many American citizens seem to quite like their government getting its way by muscular means, so long as it works and they aren't inconvenienced
Many, but not all.
Moreover, his main issues (enshittification, mass surveillance, and control) are affecting Americans to the extent many are starting to notice, so Doctorow could probably get a majority on his side.
only to say that having the citizens of a foreign power in charge of the internet is very likely to cause issues no matter which power that is, because people are people
Yes, but Doctorow doesn’t make the general argument that Canada and Europe can’t rely on a foreign internet, only an American internet.
It's the wording.
The proposals are fine. "The Internet is dominated by the US government and Big Tech" and "Europe can't rely on a service largely controlled by a foreign country" would be fine. I'd even accept a fig leaf, if he mentioned "not all Americans" somewhere (keeping the "American internet" and other borderline phrases).
The problem is he says things like "the American internet" and "We’ve known the Americans couldn’t be trusted to run our internet for decades", not distinguishing between the US government-technology complex and lowly American citizens. It's subtle; while he never explicitly criticizes lowly citizens, "Americans" implicitly includes them, and he doesn't address this inclusion (e.g. with a fig leaf). And many of these citizens aren't to blame for any action he criticizes: they're actively opposing the US government and Big Tech. Doctorow is throwing these allies under the bus, to appease a rising Canadian xenophobia towards Americans, which is a poor response to manufactured American xenophobia towards Canadians.
Brainwavez
28d ago
There's something nice about having one canon, like how it can be more fun to play Minecraft in Survival Mode than Creative Mode.
But not everyone feels this way (like how some people only play Creative Mode), mainstream canons (especially today) are generally mediocre at best (even according to the mainstream audience), and IP has so many other downsides. People who want this can resort to subscribing to some curation group who picks one canon for every popular media.
Brainwavez
28d ago
'Fan fiction' could just become the norm a decade after a story gets told. Which would be a great change.
I want to point out, this is a flaw and reason why IP actually does encourage creativity: it's already bad that people keep reusing tropes because they're reliable, encouraging experimentation (even by coercion) leads to better works in the long run.
But IP has so many other downsides, sometimes it even discourages and blocks original works (for example, LLMs being broadly censored against anything resembling IP, because otherwise it's too easy to trick them into generating it). And it turns out, fan-fiction writers are often more creative than original fiction writers, by applying creativity to less common aspects (besides the core characters/settings/etc. which they reused).
Brainwavez
28d ago
If they have $100 million, they can create their own brand with slightly different details, so it steals ideas from the existing brand without violating its copyright, and succeed off marketing even if their brand is worse.
In both cases, the original creator probably ends up with more sales and attention than they would've otherwise, by being credited with inspiring the heavily-marketed release.
Brainwavez
28d ago
Unless you have planned from the beginning for the idea that your game should be runnable without access to a server or that your server must be runnable on random consumer hardware I can see why it would be pretty difficult to backport that capability
Hence I don't think they should be obligated to backport it, just that users shouldn't be prevented from reverse-engineering the software and backporting it themselves.
It sounds like Office 2019 for Mac shipped with a local certificate that does the verification of license keys. Microsoft has renewed that certificate but distributing the renewed certificate still requires an update to the software containing the certificate. Microsoft isn't releasing an update for Office 2019 since it has been out of support for 3 years. If they no longer have the source code this may be very difficult to do. They should not have made representations that it would work in perpetuity knowing this limitation.
Similarly, someone will definitely figure out how to patch the certificate if they haven't already done so.
But here, Microsoft is a trillion-dollar company and explicitly promised the software would continue to function, so I think they should be obligated.
I find it funny that this law seems like it could easily be more punitive to companies I think are much more pro-consumer than those that are anti-consumer, due to the subscription carve-out.
Another reason why I prefer removing regulations over adding them.
Brainwavez
28d ago
Why extend to life of the author?
As I understand, the main benefit of copyright is to get authors paid for works that are physically free to copy. They should be paid, or many people won’t be incentivized or able to afford creating such works.
But why should they continue to be paid after a few years, when they haven’t done anything else productive (if they did, for example created another work, they’ll be paid from that).
if we're going to be pedantic, proofs of kind Prop are irrelevant
If someone's "proofs" aren't of kind Prop, they're doing something wrong.
And irrelevance implies interchangeability: the definition
proof_irrel : ∀ {a : Prop} (h₁ h₂ : a), h₁ = h₂
combined with a property of equality
Eq.subst : ∀ {α : Sort u} {motive : α → Prop} {a b : α}, a = b → motive a → motive b
allow substituting a proof with any other of the same theorem.
Brainwavez
28d ago
Copyrights should expire much sooner, a few years at most. I can't imagine any serious drawback.
Let's talk about software revocation: when a seller limits or disables their software after release, like an online game shuts down, particularly when customers aren't refunded.
Examples
Egregious example: Microsoft plans to remotely disable Office 2019 and 2021 for Mac. To be clear, this software was a one-time purchase and works completely offline, Microsoft even explicitly stated at one point it would continue to function. I can't even play devil's advocate.
Another example that I personally believe is stupid: when music from games is removed because the songs are licensed for a fixed duration (e.g. GTA4). Because, why include songs with these licensing requirements, when there are plenty of great songs without them? (And I don't think the removed songs from the GTA4 list are especially popular, I don't recognize any of them and only a couple artists.) Many games are simply delisted when the licenses expire; alternatively the licensed songs could be gated only for new users. At least these gamers weren't explicitly told the music would last forever (I assume), they just assumed.
Less egregious cases: when online-only games shut down. It's expensive to keep servers running; if the seller is an individual or small company they may obviously not have the funds. Providing users self-hostable servers can also be expensive: the server code should be changed for consumer hardware and documented, and the client code should be changed with UX and functionality for custom servers, or gamers will have trouble running it. Sometimes, the seller legally can't release server binaries, for IP reasons I don't really understand (the client code has third-party libraries, why is the server code different?). The most justified cases (albeit rare): the game is free-to-play with only temporary (e.g. seasonal) micro transactions, so there's nothing to refund.
The archtypal example: The Crew. A paid game released (by Ubisoft) in 2014 and permanently shut down in 2024 (without refunds). Online was a big part of the core gameplay, but the game had an offline mode which included a single-player campaign. Regardless, when Ubisoft shut down the game, they disabled the online mode and stopped players from re-downloading it. This shutdown spawned Stop Killing Games and lots of discussion about software revocation. Fortunately, the community has created a mod that re-enables the game and emulates its server (The Crew Unlimited).
Reactions
Stop Killing games campaign/NGO (mentioned above). Most known for collecting 1 million EU signatures so the EU Commission must eventually discuss their initiative, they also collected enough UK signatures for a UK parliament debate, and lobby in the US. Their voice has reached mainstream audiences (more or less: the world is so complicated there's not really one mainstream, but besides millions of signatures, they also got endorsed by celebrities including PewDiePie and Notch), but they haven't (physically) accomplished much, yet...
California's Protect our Games act. Passed the state assembly (not yet law). It requires publishers to post a notice 60 days before shutting down their game, and provide some offline functionality or refunds, although it doesn't apply to subscription games (and may have other exceptions). Backed by Stop Killing Games.
French consumer group sues Ubisoft over shutdown of online game 'The Crew': "UFC-Que Choisir alleges that Ubisoft misled consumers about the permanence of their purchase and imposed abusive contractual clauses stripping players of ownership rights". An earlier lawsuit in the US was dismissed. Backed by Stop Killing Games.
Cory Doctorow has (of course) written about this. I still support his crusade against enshittification, centralization, and unreasonable DRM (regardless of underlying goals), but I admit my general opinion of him has lowered, as this recent article has subtle xenophobia.
A road paved with good intentions
Of course consumers shouldn't lose access to things they've bought. You wouldn't remotely shutdown a car, or remotely disable its heating, or make previously-free heating a paid upgrade...(In fairness, the first two were mandated by governments, and the third was walked back.) Back on topic, surely at least egregious cases like Microsoft's are unjustified, so why shouldn't we prevent them via regulation?
It's not so simple:
-
Generally speaking: regulation doesn't intrinsically prevent anything, it's just a strongly-worded suggestion to the government and population. Moreover, all regulations have drawbacks: they cost money to enforce, discourage businesses, and hurt good-intentioned violators. Selective enforcement leads to the worse of both, where good-intentioned individuals and small businesses are targeted (sometimes frivolously but it still hurts them) while big businesses are ignored; an example I think is copyright, with false DMCA claims hurting individuals while big AI companies train on everything.
-
Consider the regulation "a software seller cannot disable any offline feature in their client without refunding buyers". Sounds reasonable, right? But what if an indie game developer pushes a balance chance that nerfs an OP character by removing their special ability? What if they remove a poorly-implemented game mode almost nobody was playing? Both of these also sound reasonable, but both can be considered disabling offline features. Even if no indie is successfully sued for such a frivolous reason, a failed lawsuit (motivated by the law) would harm them; even if there's no real lawsuit, the potential may discourage them.
My proposal
For now, media pushback and patches seem to be working for the most egregious cases. The Crew is playable via mod, more games are explicitly stating they won't remove licensed songs, I predict Microsoft will walk back revoking Office and am confident otherwise there will be a widely-available patch.
For the future, I support removing regulations on buyers circumventing end-of-life software, rather than adding regulations on sellers. At least after software becomes "end-of-life" (but preferably in general), there should be no restrictions on hacking the local version, only trying to hack the server. This won't stop determined sellers who put the entire game on the server and don't stream important gameplay logic (effectively recreating Stadia for only their game); but it's an improvement, and that streaming would make their game accessible to gamers with low-end PCs.
Your general argument is correct, because proofs won't scale without efficient tactics and smart sub-lemmas, which can't be algorithmically verified.
But Cunningham's Law obligates me to point out that proofs are interchangeable, it's called proof irrelevance. A value is basically only considered a proof if it's type's type is Prop, and once the proof is verified (i.e. value is type-checked), Lean can forget it and only remember that the theorem is proven (i.e. type is inhabited).
Brainwavez
29d ago
But this general argument (ChatGPT can claim something in English, then formally prove something completely different) still applies if the proofs are classical.
I’m confident Terrace Tao is pro-AI both because it funds him and he finds it interesting and potentially useful. That’s academia (usually).
OpenAI’s model did solve a long-standing Erdos problem (not in Lean, hand-checked by mathematicians, but still)
They promised the software would “continue to function”, yet they’re the ones who set the certificate to expire and now refuse to update it.
It’s not their responsibility to update the software further, including not their responsibility to fix if Apple breaks the software via OS update (although they should let someone else fix it).
It’s selling someone a product with a built-in unadvertised kill switch (planned obsolescence without plausible deniability). The seller isn’t responsible for reasonable defects outside the warranty, nor if the buyer breaks the product. But if they put in an unreasonable kill switch (from malice or incompetence) they’re responsible, even outside the warranty. DRM that expires and bricks the software (which no other DRM I’m aware of does) is an unreasonable kill switch.
More options
Context Copy link