Positive note from me: one thing I've had good experience with is following the path from a project that does something similar to what I want; extract a tech-neutral prose spec from the source; convert that prose spec into a formal spec; use that spec to generate valid traces, a language-specific interface layer, and conformance checks to test whether an implementation of the interface generates good traces. Once you've got that, implementing the system is a matter of colouring the interface in by numbers, which is really easy for a model.

The bonus here is that you can cut in at the prose spec stage and change it to whatever you need, as well as being able to target it at specific technical choices at the last couple of steps.

Where I've seen this work really well is with privilege escalation management, where you do actually want to be careful about the states the system can get into, and the APIs available for managing privileges in a system might be super specific to that system. But I can imagine the workflow being quite a useful one any time you've got anything state-machine flavoured.

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.

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.