danabramov

It works on the type system level instead of at runtime. So you don't actually need to "run" any code to verify it, and you can verify it for all possible inputs, even infinity of them, rather than for the ones that exist in your test.

Lean is super cool. If you're curious how proof checking works (on the type system level), I wrote an article about that: https://overreacted.io/beyond-booleans/

Here's another article I wrote that gives some intuition about the role of axioms in Lean: https://overreacted.io/the-math-is-haunted/

And here's a longer primer on Lean's syntax: https://overreacted.io/a-lean-syntax-primer/

Finally, if this got this even a little bit curious, I strongly encourage you to play the Natural Number Game: https://adam.math.hhu.de/#/g/leanprover-community/nng4

This is the best intro to Lean I know, plus it teaches you why a + b = b + a.

How much do you try to understand while doing it? I.e. how many levels of abstraction down in your own understanding do you go vs vibing at the surface level?

want to give people <usename>.<domain> account

To clarify, do you mean you want their domain handles to look like this, or do you want to make them all have `did:web` identities? These are two different questions. Domain handles would work either way (with `did:plc` or `did:web`).

Indeed, the choice between `did:plc` and `did:web` is precisely "would I rather host tie identity JSON document to an entry in a centralized open source publicly verifiable registry that is moving to be maintained as neutrally as possible, or would I rather choose to tie my identity JSON document to a domain". And that choice has to be done at the account creation because every DID, by design, is immutable.

What options are lacking in that choice? It feels like it has an option for a pragmatist and an option for a purist.

Ergo, did:web does not provide the same UX as did:plc

I mean, that is the difference between them. `did:web` means "I don't want to depend on anyone except domain authorities; I'm fine with losing identity if I lose the domain". Choosing `did:plc` means "I'm okay with depending on a central registry and find the threat model around it acceptable; I never worry about losing a domain". Both options are available.

Let me try to explain my position.

The parent post says "the only viable instance" which implicitly packs an assumption of Mastodon-like topology: a single product is expected to be split into many "instances", with some of them being more or less "viable", and that a lack of many "viable" "instances" is perceived as the protocol not being a real thing, or failing to live up to its promise. (How else are you reading "viable instance"?)

I believe that if you look at the network topology, this argument becomes much closer to "Google Reader being the only viable instance of Google Reader means RSS is a scam with a single player". Which is an absurd thing to say. That is what I'm trying to show by picking at the word "instance".

Do you find my argument flawed, or just the way I present it? How do you prefer I present it alternatively? And how do you read the parent post? My issue isn't with the word, but with the implication in the parent post.

I'll try to mention it once per discussion page in the future. Also, I have not been working at Bluesky for over a year. While I was there, I was working on the client app and not the protocol. In fact, initially I thought the protocol stuff was a bunch of nonsense.

I did read your post :) Yes, you can't migrate between PLC and WEB methods. It's not possible. I get that it's frustrating if you learn about it after making an account. Is that the whole concern?

I was replying to this:

not being able to self host a true alternative to did:plc has put a halt to that for now while I figure out what I want to do.

I'm saying I don't know what this means. You can fully self-host with `did:web`. Yes, it's unfortunate that you've already made an account by the time you've realized that. I think that's still different from "not being able to self host".

Unless I'm just parsing what you wrote incorrectly, which is quite possible!

If you want to run a social network on ATProto, you do need the relay and app view, and those are indeed heavy requirements, but the architecture is not the same, and it depends what you're actually trying to achieve.

Note those are not heavy requirements in any atproto-specific sense.

Running an atproto relay (at the current scale) is $30/month. If you're running a popular app, this is probably comparable with some of your SaaS subscriptions. Or you could use a community-run one or pool resources with other apps. Also, many atproto apps don't use a relay at all, and rely on a community cache like https://constellation.microcosm.blue/ instead.

Running an AppView is only as expensive as running any backend. "AppViews are expensive" is a myth extrapolated from "Running a copy of a Bluesky AppView is expensive", which is true because a Bluesky AppView is a backend server that's supposed to store and serve millions of posts. It would be expensive with any technology! Atproto isn't adding an extra tax here. Running a centralized service at the same scale would be equally expensive, and a Mastodon instance at that scale would simply not run.

If your AppView only serves your app's users (and has nothing to do with Bluesky), the cost is cheap or nonexistent. It's just a normal backend that listens to a websocket stream and writes some stuff to a database.

It probably is entirely true that different apps can spin up on atproto independently

It's true, and I want to emphasize that they need nothing to do with microblogging or Bluesky posts. I think it's important to internalize this because most discussions about Mastodon are about microblogging modality. But, say, Tangled is a git hosting with social layer (issues, PRs) on atproto. So we are really comparing fundamentally different ecosystems already. Atproto is not centered around Bluesky posts or Bluesky app; it's just that Bluesky app happens to be the biggest app built on top of atproto primitives.

This, what do you say right here, is the actual concern. This specific app (or any atproto app) appears to have significant lock-in—to the point where you identify it as "natural" that it would be so—while selling itself on decentralization.

You're starting with the Mastodon perspective of "a social network is a set of fragmented views of the network with no shared sense of identity or global aggregation/search which talk to each other" and consider it natural.

Whereas I start with the regular user's understanding of a social app — it's a place where you can come, where you can see the entire world at once, where all features (global search, recommendations, follow graph) are global by default, and where you don't "belong" to any particular community to an extent that this community can cut you off from your followers or ban you. Instead, the app is serviced by app's developers and you're at their mercy.

Now, what does atproto try to do?

From the user's point of view, it looks as the familiar "centralized" approach — apps can have global search, recommendation algorithms, there's no fragmentation. Each app is a prism over the entire network and always shows a consistent view over it. App developers do have full control over how the app presents it. There aren't 100 copies of the same app because there are 100 communities on it. This split into instances is a "Mastodon-brained" way of thinking.

However, the underlying data lives in an app-agnostic layer. So Blacksky was able to kickstart their own projection of atproto network (filtered down to Bluesky stuff since their app is initially a clone of Bluesky). It's not an easy job to make it work for billions of posts, but no Mastodon instance even tries to support that scale. Atproto makes supporting that scale possible, and then we say "oh but this is expensive". Of course it is — it's expensive to store content from millions of people with any technology. But unlike centralized services (which atproto tries to match in baseline UX expectations), it is possible to spin up alternative projections of the same network that fully participate in it, when folks have concrete reasons to do so. (For example, Blacksky is able to take different moderation decisions as a result.)

You can go further. https://reddwarf.app/ is a working app displaying Bluesky data that does not have a backend at all and does not use Bluesky (or Blacksky) API servers. Instead, it loads data directly from the hosting layer, and uses https://constellation.microcosm.blue/ network index for querying relationships (like "give me a list of likes for this post"). This is less efficient than maintaining an index (so it loads a bit slower) but it's totally a workable model. The Constellation index itself, if I'm not mistaken, runs on someone's Raspberry Pi.

Of course, you can also "scale down" atproto to make it apples-to-apples with Mastodon. You'd add some code that filters down events only to those that are "relevant" to people who are "on" your "server" and their follows. This would be a "small world" atproto that would be easy for anyone to spin up. It's not very exciting but I guess we'll see more experiments in that area as people realize it is possible. But it's also just less exciting because you can also run the real thing if you're motivated enough. And the fact that anyone can choose to do it if there's a real need means people don't create a 1000 of shallow Bluesky clones. It just doesn't solve any actual problems other than trying to win arguments like this.

I don't think "decentralization" is a super useful prism to think about atproto. Atproto is a high scale syndication protocol, like typed signed RSS via HTTP and WebSockets with a shared data model and identity upstreamed into the web. This protocol enables independent apps, independent hosting providers, and independent caches and relays to build and participate in a shared ecosystem. That ecosystem lives on the web, so it's "decentralized" in the same sense that web itself is. But it doesn't mean that each product must be split into a thousand pieces at the UX level.

designed it around their index as the primary means of accessing anything on the web

That doesn't actually translate from the analogy though.

You don't use Bluesky to access other apps' data on atproto, you use those apps. You go to https://tangled.org/ for Tangled (atproto github), you go to https://leaflet.pub/ for Leaflet (one of atproto blogging platforms), and so on. Bluesky is not a "one stop shop" for all atproto stuff, it's just one of atproto apps, and anyone can make their own app.

The apps themselves have to compete on their own merit, completely unrelated to the protocol stuff. The protocol just makes them all interoperable and changes market dynamics (e.g. someone can resurrect a dead app by creating a new projection of existing data). If your criticism is that there aren't many apps on atproto yet — fair, but you can make those! People are making those. This is something you can actively contribute to, there's no permission you need to ask.

The "Bluesky index" is the index of Bluesky posts, so naturally you access that primarily through the Bluesky app. (Although even that isn't set in stone — see Blacksky who run their own stack for everything, but also show Bluesky posts.) And then, if you make your own app with your own data types, it would not be related to Bluesky in any way.

But in the 2020s, after watching what Google did to the web without being able to control the protocol from the beginning, a comparison of Bluesky to Google doesn't really assuage the concern people have about centralization.

Sure, and is your argument that it's better if the web had never happened? Atproto is going to IETF so it will become a "proper" internet standard. The way you shift the balance of power is by building your own stuff on it.

Are you going to write it below my every comment? I've already replied to this here: https://news.ycombinator.com/item?id=48933050. Also, I don't think either claim in my reply is dependent on who wrote it. You can trivially verify them yourself.

I haven't worked at Bluesky for over a year now. I'm genuinely excited about the protocol, and have written a bunch of things about it while I had free time between jobs. (Ironically I had no time to write about it while at Bluesky because I was too busy working around React Native bugs.)

it's impossible to actually participate in Bluesky using an alternative relay

I don't know what you mean by this. https://blacksky.community/ is definitely running their own relay. Here's a community listing of some relays: https://atproto.at/relays.

Here's an example of connecting to one of them: https://pdsls.dev/firehose?instance=wss%3A%2F%2Feurope.fireh.... From an app's perspective, they're completely interchangeable, so as an app developer you can switch to any relay you want, or run your own.

Many apps don't even use a relay at all, instead relying on caches like https://constellation.microcosm.blue/.

I don't mean it as a linguistic gotcha ("ha, you said instances! but we call them something else"). I'm saying this is a category error because the network topology is different. This is like saying that web is not free because people aren't running Google-scale indexes in their garages.

Tried to clarify this here: https://news.ycombinator.com/item?id=48932956

If you have concrete counterarguments to what I said in my articles, I would be happy to debate these counterarguments here.

I don't know what you mean by this. You absolutely can self-host all your data on your own. And if you also don't want to rely on PLC for identity, you make a `did:web` identity, and then you're completely decoupled from Bluesky-operated infra.

The reason is that "why aren't many people running Bluesky instances" is a loaded question — it presupposes that's something you should expect. But it's like asking "why aren't many people running Google". It's expensive to store billions of posts!

This is usually compared to Mastodon, but it's not apples to apples since "running a Mastodon instance" always mean a tiny partial view of the network. You can do a partial view of atproto too for the same cost, it's just not very interesting because what's the point? Every app can "see" the entire network (unlike in ActivityPub) so there's a lot less motivation to create these fragmented views into it.

I've already linked elsewhere, but I've written an article on precisely this topic, curious to see if this can clarify it for you: https://overreacted.io/there-are-no-instances-in-atproto/#so...

First off, Bluesky doesn't offer any GUI tools for PDS migration. If you want to get off their PDS, you'll need to bust out command-line tools and possibly do some steps in advance of when you need to migrate in order for everything to work properly.

This is getting much better recently. I migrated to https://eurosky.tech/accounts/ with no command line — just needed to wait for a wizard in my browser to move my records. It could've been much faster and seamless (the app was confused after this and I had to re-login), but it's definitely accessible to non-technical people, and the share of independent hosting is growing.

It's a different network topology. ActivityPub couples three things into one box: community, hosting, and an app.

Atproto decouples them: there's app-agnostic hosting (which anyone can run), and there's hosting-agnostic apps (which anyone can run).

I wrote about it here: https://overreacted.io/there-are-no-instances-in-atproto/#so...

The solution to that is to create more apps, and for one of them to become more popular. This is entirely in our hands as developers.

that also runs the only viable instance?

This is a category error. There are no "instances" in atproto.

https://overreacted.io/there-are-no-instances-in-atproto/

It segments the network differently (into "hosting" and "apps"), and on both axes anyone can run their independent app-agnostic hosting, as well as an independent hosting-agnostic app.

Cool people use ActivityPub.

ActivityPub solves a completely different (arguably, smaller) set of problems. This is like saying "Cool people use email instead of web".

I have a few diagrams here that may help see just how different they are: https://overreacted.io/there-are-no-instances-in-atproto/#so...

Single vendor owned & controlled standards always turn out badly, just a question when.

Yeah, which is why atproto is going to IETF: https://atproto.com/blog/kicking-off-the-atp-working-group. You can join the mailing list to participate in the discussions: https://mailarchive.ietf.org/arch/browse/atp/?gbt=1&index=.

Kagi's are good, yes. The issue is with Google's.

I can reproduce the same in incognito mode.

This is not true. I regularly get HN front page hits, and still use em dashes. Nobody accuses me of AI writing. Writing with em dashes is not a problem if you have something to say.

There is this one! Though I have not tested it. https://github.com/stephenturner/skill-deslop

I found it funny to just read through.

Please please please write your own blogposts. I already read “but here’s the biggest unlock, and it’s the part that’s hardest to see” all day.

I just don’t understand why undermine your own announcements by delegating comms to the machine. It’s disrespectful to the reader.

In practice, "what's actually best for the community" (growing a community of engaged engineers who feel listened to and who understand what you're doing) is not necessarily easy to show by metrics. I think the author is making a subtler point that, even if you don't hate DevRel work, the most useful kind of work is often unappreciated or devalued by decision makers.

I think so, maybe.

Rendered Markdown: https://github.com/bluesky-social/proposals/blob/permissione...

Note this is an early draft and will likely change, as PR description says.

You claim that only 2 groups are taught when 3 get taught.

I skipped the handful of exceptions because they have no rules associated with them, you just have to memorize them. Yes, it would be 3 if I counted exceptions. I am aware that they exist; you can check their list at the end of my post.

You claim that you are given arbitrary tables to memorize, but it's usually explained to foreigners that you replace the last romaji to i when conjugating the verb into -masu form.

I must have been unlucky. I don't remember what resource I was using but it was primarily teaching with a separate table per suffix. Maybe the pattern was called out but I missed it due to feeling overwhelmed with the tables.

And based off your comment here the reason behind doing this may be you extrapolating how you first learned it to how people usually learn it.

That's fair — if most people don't stumble here because this is clearly explained, that's good, and it means I've overstated the "usually taught". I still find that I prefer the specific style of explanation where we consider the corresponding vowel a part of the suffix, like -(i)masu or -(a)nai, which is how some linguists view it. That is another part of the motivation for writing the article.