Comment by passive
8 hours ago
This seemed like a high possibility, but since our adoption of LLMs in software so far has mostly been to throw out best practices, I am skeptical that it will lead us to expanded verification.
It's like Bezos talking about how we're going to have 3 day work weeks while he makes his employees piss in a bottle.
Automated proofs do sound very neat but I think they'll be constrained to a vanishingly small set of already paranoid domains like cryptography, aerospace, etc. Everywhere else is going to spend the dividends on shipping more unvetted code faster, we're just trading discipline for velocity.
Piss bottles are easily explained by rent though. You get more productive, so the landlord ups the rent, and you have to produce more for the people owning the scarce land (your landlord, the grocery store's landlord, the farmer, etc).
Software doesn't have this scarcity dynamic. People will use LLMs to build better sounder foundations (as rust is 'better' than c) and code quality will improve as we migrate to them. You won't get screwed on your rust++ license though to the point you have to piss in bottles.
> Software doesn't have this scarcity dynamic
Time is finite. People’s problems that can be solved by software is also finite. There’s diminishing returns in improving software. Rewriting bash in rust, and then testing the result would barely help anyone. Also the real world (where inputs come from) is messy. You can have the perfect mechanism (memory safety), but that grain of sand (corrupted or unexpected data) can still make it behave erratically (wrong result).
Llm adoption has just accelerated people's tendencies. Slop generators generate more slop. They're also finding and fixing bugs that have existed for decades. The societal incentives towards slop we will have to figure out but that's not new - for folks not on that wavelength and for when we get over that impulse at some point it's good if it can also do this. Just in general so sure does write a hell of a lot of tests. If it gets good at it this could pretty easily just become part of the agent loop and we get whatever wins we can from that.
AI is the dark energy of engineering - it pushes us further apart, faster. Some of us get pushed towards slop, others towards formal spec validation, and as time goes it will be harder and harder to see each other.
A while back a knowledgeable man was a philosopher, and they could all easily talk to each other and understand. As time went we split up - we have philosophy doctors in various fields who have very little to talk about.
This happened again when the term “engineer” fractured (even before software engineering). Software engineering itself fractured, too.
And it’s happening again now.