dan

dan

@danabra.mov

the deep sea. a suitcase

67.4K followers1.3K following15.8K posts

this was very good and articulated a lot i've been feeling lately. in formalization, this effect is even more noticeable: decoherence is punished by the agent being stuck in the maze for days when otherwise it would've made progress in 30 minutes but i think this applies broadly to software

Maevyn@maevyn.codes

My thoughts on the current state of AI driven software development, why I'm no longer concerned about a runaway intelligence explosion, and what I think is a far worse outcome we could be walking into maevyn.codes/decoherence

View full thread

in a sense, a program is not its source code, but a projection of a platonic "why this idea works" hyperprogram. we usually don't see the hyperprogram the original developers/team usually maintain both. but the agents mostly engage with the projection, thereby losing the hyperprogram

by the way i'm sure others said it before, but cynically i think a large part of subsidizing subscriptions is to lure professionals into area where humans alone can no longer drive the project (middle area in the article preview image) which is .. like okay maybe we have to. i'm scared of outermost

this was very good and articulated a lot i've been feeling lately. in formalization, this effect is even more noticeable: decoherence is punished by the agent being stuck in the maze for days when otherwise it would've made progress in 30 minutes but i think this applies broadly to software

Maevyn@maevyn.codes

My thoughts on the current state of AI driven software development, why I'm no longer concerned about a runaway intelligence explosion, and what I think is a far worse outcome we could be walking into maevyn.codes/decoherence

i don't think it's unavoidable but we need better ways to make the invisible (intended constraints, seams between the system, invariants, meta knowledge about which pieces are supposed to be orthogonal) visible so the agents engage with it

dan reposted

dan reposted

I’m pleased to see soft navigations count towards LCP. This was an argument I made when I worked on Google Chrome because single page apps can provide much faster UX. Let’s say goodbye to the outdated nonsense metaphors that JS is smog or a traffic jam. It never made sense — now we have the data.

i’ve been doing some research on using Lean with AI to prove software properties (in my case, pieces of React). i’ll try to share lessons if it gets to a useful state. the main thing i’m learning is that, with this setup, proofs are *grown*. you can’t “just build them”

in my experience, AI is excelling at most technical work except for ”what is the right next problem to work on”. for now, humans still have a noticeable advantage there

dan reposted

unironically, bluesky is the social website for ML. couldn’t do this anywhere else

Jaz@jaz.sh

Okay so I've built a new Atlas, this time it lets you explore the conversations on Bluesky over the past 7 days graphically. It should update every ~6 hours and help you navigate the information environment that exists on here. I've learned a LOT about what people do here today... atlas.jazco.dev

ok i take it back Astra is good how to work with it: 1. get it to deeply understand what needs to be built. not “plan“ but like get it to be a domain nerd 2. only THEN, give it a usable past sloppy attempt and ask for excellence 3. ask it to use Sols for coding so it stays on strategy and taste

View full thread

my current rating: - 5.6 Sol: dependable workhorse, sound judgment, gets through the slog and stays on rails - Fable 5.1: bulldoze through hard problems that Sol gets stuck on or fails to see bigger picture - Astra 6: deeply understand the big picture, fundamental in-place reshaping, overseer

you also have to readjust Astra towards fidelity with whatever you initially got out of it. it has a very unhealthy bias towards execution so you need to get it back to thinking deep about stuff

ok i take it back Astra is good how to work with it: 1. get it to deeply understand what needs to be built. not “plan“ but like get it to be a domain nerd 2. only THEN, give it a usable past sloppy attempt and ask for excellence 3. ask it to use Sols for coding so it stays on strategy and taste

do NOT let Astra near code until it adopts a personality of domain nerd with high bar for excellence and taste and ideally give it something that already does what you want end-to-end but maybe badly. it’ll fix it

re last point, can somebody from frontier labs please finally drill polya’s “how to solve it” into the models thinking trace habits? “we have to shift our position again and again“ is so obvious to how humans work but models refuse to do that because they race towards the finish line! so annoying

dan@danabra.mov

5.6 Sol is my guy. best model in town right now imo. maybe not the cleverest but at least it’s relatively dependable. especially if you give it a little bit of structure on how to work

wish i could refund 95% of my Astra usage. keep giving it a chance and it fumbles but it spends tokens way faster than Sol. a very disappointing release for actual implementation work

View full thread

that said Astra seems great in the first five minutes. like analyze this and that, propose how to think about the fix etc. just can’t actually let it do the work beyond a couple of steps

5.6 Sol is my guy. best model in town right now imo. maybe not the cleverest but at least it’s relatively dependable. especially if you give it a little bit of structure on how to work

wish i could refund 95% of my Astra usage. keep giving it a chance and it fumbles but it spends tokens way faster than Sol. a very disappointing release for actual implementation work

if you leave Sol overnight with a well-chosen goal, you might wake up to it done or at least see decent progress on it. if you leave Astra overnight, you‘ll wake up to it being 20% through three different misrepresentations of your goal

my uninformed mental model of AI proofs in mathematics is that they’re like lighthouses in the fog. the fog is still there, and clearing the fog is the primary value of the discipline. the lighthouses give a bit of an orientation but don’t clear the fog on their own.

“clearing the fog“ is maybe not a great analogy because it implies there’s one concrete way something works. whereas it’s more like there’s a bunch of facts, and some are considered ”interesting if true (or false)“ because the hope is that the path reveals new path systems. a weird road helps less

annoying bsky app regression: pressing profile icon (or profile posts tab) on web no longer invalidates it

dan reposted

Frog built a wet lab for the AI model. "There," he said. "Now it can do its own experiments." "What the fuck?" said Toad

anyone hooked up Jev to any proof related stuff? can it be useful for Lean? i haven't learned much about it yet