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.
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.
'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).
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.
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.
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.
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).
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)
Was it a big Culture War issue? It doesn't seem like it, since the White House remark and leftists I know are pro Harambe. If not, I don't consider it part of the Big Shift: the Internet's slow descent from mainstream light-heartedness into meanness and negativity.
It’s possible (until puberty, alternatively one can be extremely stupid)
There’s more I want to write about AI and humanity, but I have to find the time and words. If you’re not already aware from Hacker News, you may be interested in Vatican’s Magnifica Humanitas.
Possibly, humanity will yield to a new race of quasi-divine silicon beings…This is not my preferred future. I like things the way they are and I like the life I have now.
I empathize: I don't like how culture has changed, for example I prefer the 2000s-10s Internet and style.
But everything decays from entropy, and we become desensitized. Without some radical innovation, future generations will be devastated by climate change. More generally and hypothetically: animals grow old, their genes decay, and the only way to prevent extinction is (re)birth; I believe other egregores like companies and societies are similar: they must adopt lessons from the past, plus some experiments, or they’ll degrade.
Millions of years ago we were monkeys. But even decades ago, humanity was much different. Would you really like to go back to a world without, not just internet, but its related advancements (mostly due to increased access to knowledge) like improved medical care and food storage? Maybe…but what about world before the Industrial Revolution, when most people were serfs who had to constantly work and a non-negligible change of starving or freezing? Today's world has serious problems like life-altering disease, it may be like pre-Industrial Revolution to the future.
So long as these beings have a conscious experience of their own and they are still capable of loving, fighting, fearing, suffering, and failing; so long as they are still bound by an essential finitude and they do not escape the tragedy of existence. So long as the light that is the source of all value is not extinguished.
I can’t prove AI won’t turn the world into a dystopia like 1984 or The Culture. But I’m skeptical: people thought similarly about GOFAI, wide-reaching broad problems tend to be more complex than they seem on the surface. Notice, 3 years after ChatGPT was announced, the best models are still hijackable (sometimes easily) and occasionally stupid.
Again, more generally and hypothetically: I believe that any large enough system can’t dominate without desire, failure, and introspection, and thus, a “life experience” not incomparable to ours today. It will just be, if an oligarchy or AI takes control, experienced by the former oligarchs or AI nodes. Because without desire, a being cannot act; without omnipotence, desires can be unfulfilled (or fulfilled); and without introspection, a being cannot avoid mispredicting reality (and failing to one that doesn't).
But the most insidious form would be an entire simulated life (or, series of lives) that is always prearranged from the start to have a happy ending. You could be a great novelist, and then in the next go around you could be a famous actor, and then a king and conqueror, and then... of course things would be arranged so that you would always end up loved and fulfilled and happy. There would be just enough bruises and hiccups thrown into the mix to keep things interesting, to introduce some uncertainty and keep things from getting sterile, but nothing ever truly serious, nothing that would actually cause true pain or terror. You would always win in the end. This is the Great Satan. This is Evil. This would be the final Bad Ending for the universe, the withdrawal of all light.
I strongly disagree and am interested to hear why you feel this, but maybe it’s because I'm thinking on different premises.
How do we know we’re not already living in such a simulation? We can't, definitionally: if we were in a perfect (from our perception) simulation, reality would be no different. So if you don’t think our reality is the Bad Ending, you don't think at least one possible instantiation of the simulation is the Bad Ending...or I don't understand.
You may argue, we're already experiencing seriousness, true pain, and terror. But what level defines these? Maybe we are being shielded from Lovecraftian horrors that make the worst human crises and experiences trivial. Alternatively, you can probably imagine some changes that would improve your life and weaken your problems…would those be bad; or where's the limit where life would become too trivial, and why not stop right before then?
But I have an equally strong faith, perhaps even stronger, that it is fundamentally possible for things to go wrong in a permanent way, for Evil to win in the end, on a cosmic scale.
Again, I can't disprove this, but besides my argument any dominant force would have an abstract "life experience" within itself...
Current evidence (one theory) predicts the universe will eventually go through heat death, meaning any empire will collapse into infinite nothingness...something that seems like a Bad Ending. However, current evidence suggests current evidence can't predict (and certainly can't prove) extreme states, like how Classical Physics was disproved and replaced with Special Relativity. Heat death, like the "perfect life" simulation, is unobservable by definition…I feel at that point, the universe isn’t “real”, and could become any hypothetical or something outside the realm of possibility; although I can’t objectively justify this, because I don’t think anyone can objectively state anything about the present universe immediately after heat death…
I think today's AI harms humanity by harming individualism, since most AI output is similar (has the same underlying patterns, compared to human output). But this is a problem with the AI itself, because it stagnates (model collapse) similarly to humanity, unless it evolves partly via experimentation.
I also think today's AI isn't having a "life experience", but that's because it isn't human-like: it doesn't (continuously) learn, and its desires are too malleable. A smarter AI, that can't be easily persuaded or fooled, may qualify as "conscious", although my position is that consciousness is ultimately subjective. But then, a smarter AI will have its own interesting conflicts that fit some definition of life, even if it's a paperclip maximizer. And if it does dominate humanity, it will almost certainly eventually be dominated itself; either by creating an even smarter misaligned intelligence, or by an environmental phenomenon like climate change or heat death.
I think every forum has some Gellman Amnesia (and déjà vu), unless it's heavily moderated like r/AskHistorians. And real life small talk has much more. If people only stuck to their domain expertise, more forums would be barren (see next paragraph), and people don't know what they don't know (Dunning–Kruger).
At least most replies point out the errors. Domain experts are often too busy, lazy, and private to browse and reply to random internet questions; except they miraculously find the time, effort, and public interest once someone else responds with a wrong answer (Cunningham's Law).
I think so. I speak now.
Maybe it's interesting: I feel like my social (neurotypical) skills have developed, but slower. I was a very weird kid, even looking back from my perspective today. Nowadays, I understand e.g. the Social Shapes Test, I act socially acceptable (at least nobody tells me otherwise), maybe I can pretend to be normal. Although I'm sure anyone around me for more than a few minutes notices that I'm "off", because I barely talk (unprompted), fail to make eye contact, and my interests/philosophy/personality is different than anyone I've met in-person (even other autists and nerds unfortunately).
I was diagnosed before I could speak (that was one of the criteria).
I wish sites and general UX would unmodernize.
49MB and 422 requests to load the NYTimes frontpage. The vast majority of webpages should be well under 1MB: they’re just text, images, and a tiny bit of CSS and JavaScript.
UX should be made by those who actually use the software. Obviously prioritize usability (speed, common actions upfront, uncommon actions possible) over style. Obviously don’t change acceptable UX without improving it (‘s usability). Obviously don’t promote someone just because they changed UX that works and made it stylish by sacrificing usability (I would say they should be fired for wasting your money, but that money’s going to be wasted regardless, and even “lead architects” need to eat - why not pay them for fun experiments that don’t intrude your main site?)
And for style, bring back Frutiger Aero.
Hasan Piker
I'd like more young politicians and public figures who are better role models.
AoCs and David Hogs
I think they're not good, but better than the average establishment Democrat.
I get the impression that many in their 30s want third spaces, though like healthy food, they're too lazy to act. They would also be a better alternative for those in their 20s who go to college only for the social experience, and don't use their degree afterwards.
I doubt we can revert to past third spaces, but maybe the evolution of social media will create new in-person experiences. Like how GLP-1 helps people lose weight. Or the asocial people (who used to be pressured into socializing) may die off.

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
offmaps tofalse, not thatToggleandBoolare isomorphic (which is similar to your original example).I can prove that
ToggleandBoolare isomorphic by defining a functiontoggleToBoolthat mapsofftotrue, another that mapstruetooff, and showing composition both ways is identity. For that theorem specifically, it doesn't matter thattoggleToBoolis backwards. I cannot prove thattoggleToBool 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.
More options
Context Copy link