What I'm building in Cairn, one milestone at a time. Each post says what the milestone set out to show and what it still can't, with videos of the work as it landed.
-
Likes that show at once and end up true
Sky can now like, repost, follow and mute. Each act shows the moment you press it, and a proof says the counts end up matching the server's, whatever order its replies come in.
-
A feed that never ends
Sky signs in to Bluesky, keeps the session in the Keychain and reads the home feed however long it gets. It's built only from registry packages.
-
An app built from packages alone
Pairs is a memory game built only through Cairn's package path, with images, JSON and requests in flight that it doesn't control.
-
Claims on an app I use every day
I rebuilt Yap, my dictation app, on Cairn. The global key, the microphone, timers and typing into other apps are all effects Lean asks for.
-
A proved TodoMVC
TodoMVC on the Mac, written in Lean, with every action a claim and proofs that each control is on screen exactly when it should be and can be pressed.