Likes that show at once and end up true

2026-10-26Milestone 5, in progress

Sky, the Bluesky client I'm building on Cairn, could read a feed. Now it can act on one: like, repost, follow and mute, with a notifications tab beside Home. This is the fifth milestone, and it's still in progress.

The hard part of a like button isn't drawing it. The button has to change the instant you press it, before the server has answered, and the server may refuse, answer late, answer out of order, or act and lose the reply. Most apps handle that with care and hope. I wanted a claim:

Once every reply is in, whatever order the replies came in, each post shows what the server holds, and its count is the server's.

What Cairn gained

Optimistic values (Cairn.Optimistic): keyed values shown at once, with one write in flight per key. A refused write rolls back in the step its answer arrives, and a lost reply is read back. The convergence proof is about the framework, so every app gets it, not just Sky.
Menus on controls and on the secondary click, and an app's own items in the menu bar.
scrollTo, the Dock badge and spoken announcements, as effects the host runs.
A server with a world of its own in cairn fuzz. It keeps the likes and follows, loses replies after acting on them, and lets the fuzzer check claims against what it holds.
cairn_atproto 0.3.0: record keys, idempotent writes, the authoritative read, viewer state and notifications.

What it looks like

When the server refuses a like, Sky rolls it back, says so in a line and announces it to VoiceOver. Muting an author takes their posts out of the feed at once without moving the post you're reading, and the status line offers Undo. Notifications are grouped ("Alice, Bob and 3 others liked your post"), counted on the tab and the Dock, and marked seen once they're on screen.

The catch

The proof is about a model of the server: one register per key, with idempotent writes. Bluesky's real servers lag, so a count other people are changing can be briefly behind; the count claim holds when no one else has acted since the last view. Posting, replies and quotes are the next milestone.

Progress log

The videos and notes from this milestone as the work landed, newest first.

Try it, back in the browser
TodoMVC from cairn_examples on /try/todo/: every frame one its Lean code drew, captured headless by make try. The pointer is on a todo's checkbox, cairn_examples^204, proved, with its claim page a click away.
2026-10-26dccde9a0
Sky: the notifications list
Grouped likes, follows with Follow back, replies and mentions as posts with Like, Repost and ⋯; the unread count on the tab.
2026-10-26a85a11f0
Sky: notifications on screen
Others like, repost and follow while the reader is on Home: the count comes onto the Notifications tab (and the Dock badge). The tab opens the list, "3 new" takes it to the new rows, which are marked seen; Follow back, a like from a mention, then Home again at the same place. Rendered offscreen against the fake PDS.
2026-10-26a85a11f016s
Cairn 0.5.2
Cairn 0.5.2 is out on the public registry with two virtual-list fixes Sky turned up: a list now settles however many layouts it takes when many rows it knows change height at once (Sky's mute hiding many posts), and a clamp within a batch no longer moves the reader's row when a later step of the same batch lengthens the list.
No claim is new, retired, moved or changed. The registry's ledger check accepted 0.5.1 to 0.5.2 and serves its claims export for the claim pages.
2026-10-2623f0836
Sky: muting an author mid-feed
⋯ on a post, Mute: the author's posts leave the feed and the post being read stays where it is; the status line offers Undo, which brings them back (cairn#254). The ⋯ menu is AppKit's and isn't in the offscreen render: the button shows pressed while it is open.
2026-10-26f9a66b658s
Sky: Like and Repost, one refused
Sky against the fake PDS with its replies slowed by 1.4 s: Like shows at once and greys until the server confirms it, then Repost; the next Like is refused and rolls back, with the reason in the status line (cairn#254). Rendered offscreen from the engine's frames.
2026-10-26f9a66b6511s
Cairn 0.5.1
Cairn 0.5.1 is out on the public registry: cairn conformance now holds the world (the debug socket's holdWorld stops the host's own clock, wake and requests, and the driver decides the time and every reply), benchmarks for Cairn.Optimistic up to 1,000,000 keys, and two fixes Sky needs: cairn fuzz no longer treats controls as hidden after a virtual list is replaced, and a held clock never steps an app with an empty batch.
One claim is new, ^1032 (under holdWorld the host sends no clock, wake or reply of its own), fuzzed by world.hold. The registry's ledger check accepted 0.5.0 to 0.5.1 and serves its claims export for the claim pages.
2026-10-263616efd
Sky: like, repost, follow and mute
Sky's feed with the acts row under each post: Like, Repost, Follow and Mute, built on Cairn.Optimistic and cairn_atproto's writes. An offscreen render against the fake server.
2026-10-267a69f8b
Sky: notifications, grouped
Sky's notifications: likes of one post in one row, marked seen once on screen (cairn#253).
2026-10-267a69f8b
Sky: unread notifications
The unread count, polled from the fake PDS, on Sky's Notifications tab (cairn#253).
2026-10-267a69f8b
Cairn 0.5.0 and cairn_atproto 0.3.0, early in M5
Cairn 0.5.0 is out on the public registry as iamnbutler/cairn, so Sky's M5 work builds on it from the registry: Cairn.Optimistic (values shown at once, confirmed or rolled back, ^1100–^1114), a fuzz server with a world that fails requests before it acts and loses replies after, menus on controls and in the menu bar, Effect.scrollTo, kept scroll boxes, the Dock badge and announcements. Frames are v13, and every app now links Lean's libStd.
cairn_atproto 0.3.0 follows on Cairn ^0.5.0, with Fake.server: the fake PDS as a cairn fuzz server whose world is the whole PDS and the host's Keychain. A small app in the package, FakeApp, runs under cairn fuzz with it and checks that the server holds every like it acknowledged while replies are lost and tokens rotate.
The registry's ledger check accepted 0.4.1 to 0.5.0 (23 new claims, none retired) and cairn_atproto 0.2.0 to 0.3.0, and serves both claims exports for the claim pages.
2026-10-26486e8ce
Likes that roll back
The fixture's Like buttons on Cairn.Optimistic, against a scripted server: each press shows at once with its count. Post 1's like is accepted. Post 3's is refused and rolled back in the step the refusal arrives, with a line saying so. Post 4's reply is lost after the server applied it, so the post stays liked, dimmed, until the read back confirms it. Rendered offscreen (Fixture --like-frames).
2026-10-26a8d031013s