> you can't spec out something you have no clue how to build
Ideally—and at least somewhat in practice—a specification language is as much a tool for design as it is for correctness. Writing the specification lets you explore the design space of your problem quickly with feedback from the specification language itself, even before you get to implementing anything. A high-level spec lets you pin down which properties of the system actually matter, automatically finds an inconsistencies and forces you to resolve them explicitly. (This is especially important for using AI because an AI model will silently resolve inconsistencies in ways that don't always make sense but are also easy to miss!)
Then, when you do start implementing the system and inevitably find issues you missed, the specification language gives you a clear place to update your design to match your understanding. You get a concrete artifact that captures your understanding of the problem and the solution, and you can use that to keep the overall complexity of the system from getting beyond practical human comprehension.
A key insight is that formal specification absolutely does not have to be a totally up-front tool. If anything, it's a tool that makes iterating on the design of the system easier.
Traditionally, formal specification have been hard to use as design tools partly because of incidental complexity in the spec systems themselves, but mostly because of the overhead needed to not only implement the spec but also maintain a connection between the spec and the implementation. The tools that have been practical outside of specific niches are the ones that solve this connection problem. Type systems are a lightweight sort of formal verification, and the reason they took off more than other approaches is that typechecking automatically maintains the connection between the types and the rest of the code.
LLMs help smooth out the learning curve for using specification languages, and make it much easier to generate and check that implementations match the spec. There are still a lot of rough edges to work out but, to me, this absolutely seems to be the most promising direction for AI-supported system design and development in the future.
I mean, look at all the startups that succeeded despite being complete shitshows behind the scenes... the baseline for leadership, organization, coordination or, hell, execution for a startup to succeed isn't exactly high either.
Living with ADHD also increases your chances of getting into a car accident substantially. I can't find the numbers now, but the increase is non-trivial and there are some clear mechanisms (inattention, impulsivity and risk-seeking behaviors).
ADHD is a big part of the reason I don't drive. I'm lucky enough to live in Berkeley which is very walkable with decent transit, and I would hesitate to move anywhere more car-oriented exactly because I have ADHD.
Yeah, ADHD does affect one's ability to drive safely. On the other hand, I've been driving for over 50 years. I've had one accident that I was responsible for. Various other vehicles have been involved in five other accidents where the other driver backed into my parked car.
I think the reason I've been hypervigilant about safe driving practices is that my father owned a rigging company, and I was driving forklifts and stake trucks in the yard from about 13. I understood the impact a vehicle could have on other things, people included. Living in that world from about age nine on teaches you to be obsessive about properly securing a load (Molding machines, air handling units, lathes, etc.).
I've often thought people would be better drivers if they started their driving experience with the motorcycle safety training course curriculum and drove for a year on motorized two wheels, taking up the lane and keeping up with traffic.
When I was younger I was lucky enough to live somewhere rural where I got into a couple of single car accidents that I walked away from. Now my ADHD hyper focus is super attentive when driving.
There's a lot of area on the spectrum between where we are today and "sugary beverages are all banned".
For example, Starbucks could limit the sizes it sells and advertises—you'd still be able to have as much sugar as you would like by buying multiple drinks, but it would raise the activation energy needed to do that. Making the healthier choice the path of least resistance works wonders.
It's not inevitable, it's just poor leadership. I've seen changes at large organizations take without being crudely pushed top-down and you'd better believe I've seen top-down initiatives fail, so "performance management" is neither necessary nor sufficient.
> crystal clear software development plan and the exact know-how to implement it
This is simply not how expert programmers work. Programming is planning, and programming languages are surprisingly good planning tools. But, of course, becoming an expert is hard and requires not only some general aptitude but also substantial time, experience and effort.
My theory is that this is a source of diverging views on LLMs for programming: people who see programming languages as tools for thought compared to people who see programming languages as, exclusively, tools to make computers do stuff. It's no surprise that the former would see more value in programming qua programming, while the latter are happy to sweep code under the rug.
The fundamental problem, of course, is that anything worth doing in code is going to involve pinning down a massive amount of small details. Programming languages are formal systems with nice (well, somewhat nice) UX, and formal systems are great for, well, specifying details. Human text is not.
Then again, while there might be a lot of details, there are also a lot of applications where the details barely matter. So why not let a black box make all the little decisions?
The question boils down to where you want to spend more energy: developing and articulating a good conceptual model up-front, or debugging a messy system later on. And here, too, I've found programmers fall into two distinct camps, probably for the same reasons they differ in their views on LLMs.
In principle, LLM capabilities could be reasonably well-suited to the up-front thinking-oriented programming paradigm. But, in practice, none of the tools or approaches popular today—certainly none of the ones I'm familiar with—are oriented in that direction. We have a real tooling gap.
> My theory is that this is a source of diverging views on LLMs for programming: people who see programming languages as tools for thought compared to people who see programming languages as, exclusively, tools to make computers do stuff. It's no surprise that the former would see more value in programming qua programming, while the latter are happy to sweep code under the rug.
i'd postulate this: most people see llms as tools for thought. programmers also see llms as tools for programming. some programmers, right now, are getting very good at both, and are binding the two together.
Most people? I'd suggest few people see LLMs as tools for thought and more that they're slop machines being cynically forced upon workers by capitalists with dollar signs in their eyes. Over and over and over again we see real-world studies showing that the people far more excited about genAI are managers than the people doing the actual work.
Efficiency isn't even the best way to optimize for (expected) shareholder returns for an organization! Efficiency fundamentally trades-off against adaptability and resilience.
A major part of what makes somebody "the best" is tacit knowledge. This is the sort of skill and "know-how" you can build up from experience and one-on-one instruction, but cannot easily be captured in text.
For programmers, this manifests as some mix of intuition and taste. I've worked with people who have had some especial insight that most doesn't; they don't necessarily "produce" the most, but they make the right key decisions and create the kind of core abstractions and systems that provide a better foundation for everything down the line. Or, alternatively, perhaps they're just preternaturally great at finding and fixing bugs. (My experience has been that really good folks tend to lean heavily towards one side or the other, even if they're solid at both.)
I've written before about how this should change how we structure our teams and manage creative, high-leverage work[1]. The same concept should also change how we find and evaluate candidates, but, honestly, I'm not sure how. Evaluating tacit knowledge and expertise is hard, even for experts!
One thing I've found that works is figuring out a way to show-rather-than-tell that you're willing to do things differently. Doing things differently won't be appealing to everyone, but it will be very appealing to specific kinds of experts! When you can't compete on comp and brand, this is one of the better options. One way to do this is to use a specialized, niche language like Haskell. Alex saw this in action at Freckle and I saw it in action hiring folks for Target's supply chain optimization team. But it doesn't have to be a language specifically; it just has to be something that at least some experts care about, and that you can demonstrate. (Just saying you're doing something different or technically interesting won't work because everybody is saying that!)
Hey Tikhon! The Haskell thing was such a great way to filter for interesting frontier people back in the day, as we both experienced. That was a contrarian bet at the time, but it paid off handsomely for at least a few of us. The number of people we'd get to interview was only a fraction of the broader population, but it felt like 30-50% of the people we would talk to were awesome fits.
It's also pretty clearly a deterrence against people admitting and fixing their own mistakes, both individually and as institutions. Which is exactly what we're seeing here...
Ideally—and at least somewhat in practice—a specification language is as much a tool for design as it is for correctness. Writing the specification lets you explore the design space of your problem quickly with feedback from the specification language itself, even before you get to implementing anything. A high-level spec lets you pin down which properties of the system actually matter, automatically finds an inconsistencies and forces you to resolve them explicitly. (This is especially important for using AI because an AI model will silently resolve inconsistencies in ways that don't always make sense but are also easy to miss!)
Then, when you do start implementing the system and inevitably find issues you missed, the specification language gives you a clear place to update your design to match your understanding. You get a concrete artifact that captures your understanding of the problem and the solution, and you can use that to keep the overall complexity of the system from getting beyond practical human comprehension.
A key insight is that formal specification absolutely does not have to be a totally up-front tool. If anything, it's a tool that makes iterating on the design of the system easier.
Traditionally, formal specification have been hard to use as design tools partly because of incidental complexity in the spec systems themselves, but mostly because of the overhead needed to not only implement the spec but also maintain a connection between the spec and the implementation. The tools that have been practical outside of specific niches are the ones that solve this connection problem. Type systems are a lightweight sort of formal verification, and the reason they took off more than other approaches is that typechecking automatically maintains the connection between the types and the rest of the code.
LLMs help smooth out the learning curve for using specification languages, and make it much easier to generate and check that implementations match the spec. There are still a lot of rough edges to work out but, to me, this absolutely seems to be the most promising direction for AI-supported system design and development in the future.
reply