More

danabramov · 2026-09-12T01:54:19

Have you considered that different things are difficult for different people? Learning hiragana and katakana has taken me about a month, and I found it very difficult. There is no need to make it prerequisite for starting to learn grammar, forming sentences, or pronunciation.

klodolph · 2026-09-12T02:25:31

If you want to learn pronunciation you should be listening to audio.

Sure, maybe don’t force people to learn kana first. But Hepburn is kind of the worst of all worlds, it is just a waste of time to learn Hepburn.

archargelod · 2026-09-12T02:30:50

Notice how I didn't say that I "learned" both in a day, I "remembered" them. Of course actual learning will take some time, especially with less used characters. But remembering shapes and differentiating between them using mnemonics should not be too hard for most people.

danabramov · 2026-09-12T01:52:28

This is unnecessarily pedantic advice, and I encourage fellow learners of Japanese to ignore it. You will definitely need to learn hiragana and katakana but you can do it at your own pace, and it is orthogonal to learning the basics of grammar, forming sentences, and pronunciation, so you definitely don't need to think of it as an obstacle. For pronunciation in particular, obviously watching Japanese movies etc helps. And yes, I have a native Japanese teacher who recommends the same.

jimbokun · 2026-09-13T02:14:50

Learning kana is the single fastest way to internalize the Japanese phonetic system and pronunciation, in my opinion.

danabramov · 2026-08-14T21:45:31

Thanks for posting. I'm doing some AI vibemathing and running into exactly the difficulties they describe.

danabramov · 2026-08-14T12:04:03

Here's a link from the post on self-hosting this infra: https://bsky.network/docs/jetstream-self-host/

danabramov · 2026-08-10T11:41:59

Some atproto designers come (somewhat disillusioned) from the p2p world, you can read what they have to say about that here: https://atproto.com/articles/atproto-ethos#peer-to-peer and https://atproto.com/articles/atproto-ethos#synthesis

danabramov · 2026-08-10T11:39:10

>Yes, the user data is decoupled from the apps, but aren't both stored on some kind of instances?

There are two main kinds of "nodes" in atproto:

- Hosting aka "personal data servers" (PDS). This is dumb JSON hosting that you can query by HTTP or watch by Websocket. Super cheap to run. They don't talk to each other. You can have one per user, or one per many thousands.

- Apps. These are your normal webapps. (But they ingest data from everyone's hostings.) They also don't talk to each other.

So yes, there are "instances" in the sense of "boxes which run software" but the topology is completely different from Mastodon or such. Data flows from hosting into apps (and then apps write to hosting). There is no hosting-to-hosting or app-to-app connection. Hosting is app-agnostic, and apps are hosting-agnostic.

To make all of this practical, there are things in the middle that make the situation easier for app developers — either relays (which combine event stream from many hostings), or caches like Hubble[1] and Constellation[2] (which let you query the entire network in one request).

>Aren't we making some kind of federated network by deciding on our app server which event streams or which users/apps pushing updates to listen to?

Ideally you would listen to every relevant event from the entire network (and filter out every irrelevant one). It isn't hard today — you can either use an existing relay or run your own for ~$30/month or pool with someone. The discovery mechanism is that (1) a hosting can request any relay to crawl it, and (2) a relay can discover more hostings it hasn't crawled yet by following links — similar to how Google crawls the web.

[1]: https://atproto.com/blog/introducing-hubble-a-public-mirror-...

[2]: https://constellation.microcosm.blue/

danabramov · 2026-08-10T11:34:08

Shameless plug, but if this got you interested, I have a couple of longreads on the topic:

- https://overreacted.io/a-social-filesystem/

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

From the official site, I'd also recommend https://atproto.com/articles/atproto-ethos

danabramov · 2026-07-24T04:47:15

You can check yourself using https://pds.ls, just open any handle there that has Tangled repos

LelouBil · 2026-07-24T08:40:02

It's very interesting, thank you very much

https://pdsls.dev/at://did:plc:wshs7t2adsemcrrd4snkeqli/sh.t...

danabramov · 2026-07-22T12:23:36

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.

danabramov · 2026-07-22T12:03:31

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.

yboris · 2026-07-22T14:03:57

I love your posts! The Social Filesystem is amazing!

https://overreacted.io/a-social-filesystem/

nh23423fefe · 2026-07-22T13:50:44

        induction b with d hd
        rw [add_zero, zero_add]
        rfl
        rw [add_succ, succ_add]
        rw [hd]
        rfl

i really enjoyed finally internalizing dependent type theory. it helped a lot with that.