The other day, someone at work shared this article in the "AI guild" slack channel: Coding After Coders: The End of Computer Programming as We Know It
I don't really care about the article overall and I admit that I didn't read it very closely, but one quote from that article caught my eye. And kinda just made me sad. I ended up writing a response in reply. I copied most of what I wrote below. Apologies if any of this sounds too patronizing for an engineering audience, the person who shared the link is a product manager, so I wasn't sure if they would know anything about Dijkstra or the other topics. When I originally wrote it, I was also thinking about some of the more junior engineers who may read my response.
Side notes:
The reason that tech generally — and coders in particular — see L.L.M.s differently than everyone else is that in the creative disciplines, L.L.M.s take away the most soulful human parts of the work and leave the drudgery to you,” Dash says. “And in coding, L.L.M.s take away the drudgery and leave the human, soulful parts to you.
I don't have a strong opinion on the rest of the article, but this quote stood out to me. I think that mentality may be true for some people, but I'd argue that there is plenty of creativity when doing math/programming and designing technical solutions, including all those pesky details. A large source of the creativity in this endeavor is striving for elegance. One might make the analogy that coding agents are to writing programs what an electronic calculator is to performing long division by hand. Personally, I don't think it's a valid analogy. Because, in a very real sense, programming is equivalent to writing theorems (specifications) and writing proofs of those theorems. The "soulful" or even just "fun" part of math is coming up with interesting conjectures and trying to prove them true or false. A seemingly trivial looking conjecture can take quite a lot of ingenuity and thinking outside the box to figure out how to prove correctly. It's not just about executing an existing well-known set of repetitive steps like a calculator performing arithmetic algorithms (interestingly, in EWD 619 below, you'll see that Dijkstra even calls into question my framing of arithmetic here).
See this video if you're not sure what I meant by "in a very real sense", but you're interested in the relationship between programs and proofs: "Propositions as Types" by Philip Wadler. If you prefer reading, you could read this paper instead: Propositions as Types.
I'm a huge fan of Edsger W. Dijkstra, one of the greatest computer scientists to ever live. He has some interesting things to say on the topic of elegance. (Warning: he's quite infamous for coming off as arrogant and rubbing people the wrong way. Part of that is because his perspective is more as a teacher and a researcher of the boundaries of both how humans can understand computation and computation itself. At times, that is pretty far from the pragmatics of writing programs for profit, which is where most of the rest of us are).
As an aside, he was also one of the first bloggers ever. He started in the 60s, well before the term blogging was created, and there is an archive of all his "EWD"s: https://www.cs.utexas.edu/~EWD/
All that said, I think in most silicon valley style software companies, the concern is really more about pushing product and not something like mathematical or technical elegance. One of the biggest reasons for that luxury is that many of the hardest problems in computer science are solved already in the lower layers of the layered software systems we have today. Those problems are solved by systems programming (as opposed to application programming) that produced things like cryptographic libraries, databases, networking stacks, operating systems, etc. Things that we can use off the shelf nowadays instead of having to write our own before we even think about running a software based business.
The AI agents of today are standing on the shoulders of giants. Those giants are the readily available open source software that solves these more technically challenging problems along with providing tons of material for training the models.
Nothing to do with AI, since this has been a thing for a long time at this point, but it's actually quite fascinating, and some might say unfortunate, that it's much more difficult to find a job working on these lower layers that pays the kind of money that silicon valley developers working at the application layer have made for the last 10-15 years. We all know these systems are so important and valuable, but it's very difficult to gain economic rewards comparable to the value produced. On the other hand, random "apps" sell for millions or sometimes billions. Just one of those odd things in the industry.
There is plenty of ongoing research and there are early attempts at rewriting these lower level things from scratch with AI agents, but it remains to be seen if AI tools can be as successful in those domains that are both fundamentally more complex and have stronger requirements for correctness and performance.
I do think program synthesis is a worthy field of study. And that AI agents might be one of the most interesting developments in that area in recent times. The cutting edge research in this area looks pretty interesting. Some articles I've recently found and plan to read about on the subject: LLM-Guided Compositional Program Synthesis, Enhancing Program Synthesis with Large Language Models Using Many-Objective Grammar-Guided Genetic Programming, and Synergistic Utilization of LLMs for Program Synthesis.
I mention all this formal math stuff because it might become much more important to the industry at large over time. That may be of some practical interest to some developers here, especially as their long term livelihood is seemingly threatened as so many companies claim these tools replace engineers. Now that we're striving to use probabilistic code synthesis processes everywhere, it seems like we need reliable and automated ways to do things like check for correctness relative to some kind of spec, check for the equivalence of different programs, and the like. I strongly believe that in a world where it's possible to generate so much output so quickly, that curation and trust are going to become the most valuable commodity. Maybe formal methods won't end up being the first choice for solving that problem, but I think they could play a role and that industry interest in this area seemed to increase a bit recently because of LLMs and their code generation applications. That youtube video I linked above is more focused on type theory based programming languages and theorem provers, but there are other tools in the formal method space that have had more success in gaining some traction in the mainstream industry, tools like TLA+ or Alloy.
I also mention it because I think math, and thus programming, is cool and interesting in its own right.