For the first time in the history of computer science, actual practicioners of software engineering appear to be having a serious go at using automated code generation tools to produce entire programs. The industry has not yet agreed that this is an unqualified disaster.

On the other hand, we have known for quite a long time that there are a number of things that computers cannot do: not things that are merely difficult to solve, but things that are actually impossible. One particularly salient example is asking a computer program to figure out what a (possibly different) computer program even does. This raises a number of fascinating questions about the act of asking computers to write our code for us, and the roles of us as software engineers, now, and in the not-too-distant future.

We're going to focus on the act of specifying a problem, and verifying whether whether our solution to a problem meets that specification. How do we judge whether something is "correct"? How much of a problem can we ask a computer to solve? Is there still a place for not doing everything completely automatically?

This talk combines observations from foundational computer science, from the emergence of automated software testing, and some recent observations about the performance of recent-generation LLMs acting autonomously. We will raise some questions. We might answer 1-2 of them.