"What is Correct?" and is that even the right question any more? - Christopher Neugebauer - 2026

Hi, I'm Robin. Usually I'm only on stage at the very end. So, this is this is interesting and awkward. You know, the North Bay Python proposal review process is an anonymized process. And going through the process this year, there were so many proposals like no, not another talk on AI. Oh, this is an okay one. Well, one of the talks really definitely floated to the top and lo and behold, it ended up being Chris's. So, I just say that so you know, Chris earned this spot. >> [laughter] >> He's not giving himself this privilege. So, I am so happy for the first time ever to have the honor of introducing Chris. Our dear conference chair. And also a speaker and a cloud fixer-upper. Please make Chris welcome. A cloud fixer-upper is a >> [applause] >> That could almost be a professional title in this industry. Um That's not my current role. Uh Don't have one of those at the moment. But anyway, um I wanted to talk a bit today about the state of the industry which uh being in the state of relative unemployment is a a bit of a bit of a bold step. I didn't have that situation when I submitted things, but here we are. Um Shall we begin? Okay. So, the field of computing emerged in the shadow of several unsatisfying results in mathematics. In the early decades of the 20th century, the loudest voices in mathematics started on a project, the Principia Mathematica, which was an effort to starting with as little structure as possible and avoiding all externalities, methodically prove everything that was knowable about numbers. Now, having such a system would revolutionize humanity's knowledge. Every unsolved problem in arithmetic would be trivially solvable. And therefore, so would physics and therefore chemistry and therefore engineering and so on. And they went about this by way of a formal system. Formal systems are systems of logic that consist of a collection of symbols and an initial set of statements about those symbols that are the ground rules for the system. These ground rules are called axioms. Now, formal systems give rise to theorems, which are statements that are logically sound within that system. Theorems are provable if you can combine some set of axioms or other theorems in an order that gives you that theorem. In 1930, a swift halt was put to the effort to use formal systems to enumerate every theorem in arithmetic. Kurt Gödel, who's pictured here on the left alongside an unidentified physicist, delivered a result that conclusively proved that it is not possible to develop a formal system of arithmetic where every theorem was provable unless there are also valid statements that contradict each other. In the process, he showed that it was impossible to avoid externalities even in simple, abstract, ungrounded arithmetic. Gödel's result, known as the incompleteness theorem, gave rise to two important results in the following years. The first was in 1933, Tarski's undefinability theorem, which uses some techniques of Gödel's to prove that any formal system that has both enough expressiveness to perform arithmetic and a universal concept of truth within that system has the facility to construct a statement like the one on the screen here. Now, it should be clear to even even the least mathematically inclined amongst us that this concept of truth is not useful in any way. The consequence of this result is that any useful definition in any useful sort of formal system must live outside of the system itself. Logic and its interpretations are necessarily separate things. And in 1936, Alan Turing gave several results about what things can be computed. As well as literally inventing the computer by way of a formal system, he proved that there is no computer program that can, without fail, detect the existence of an infinite loop within another computer program. This is known as the halting problem. The second proof in Turing's thesis is a bit more practically troubling. He found that no computer program can determine whether another computer program will output some specific output during its execution. Now, both proofs are quite simple and they're general enough that can be extended to a lot of things. Indeed, some 17 years later, H.G. Rice, no relation to Benno, showed that Turing's second proof applies to a lot of things about computer programs. It's not just what any given program outputs that you can't determine ahead of time. It's actually any interesting behavior at all. In short, you can't tell what most programs do just by looking at it. And instead, you have to run them and observe them before you can draw any conclusions. The year is 1953 and what we have is a mess. There are some things that are true, but we can't independently verify their truth, most importantly truth itself. And in the same paper that literally invented the computer, we gained the knowledge that computer programs generally can't determine what other computer programs do. In short, programming languages are limited in what they can achieve. But what do those limits mean for computer programs? Well, there's value in starting in a with a formal systems approach. Because programming languages themselves are formal systems. They're a string of symbols that you can string together and make valid statements with. And since we have actual computers, not just ones written down on paper, we actually make tools that verify whether something is a valid statement in a programming language. And to make those tools, we have formal systems, which we can use to define the grammars of our programming languages. This idea was popularized by formal systems academics Backus and Naur, who came up with a system called Backus-Naur form. And that allows you to specify the grammar of your programming language without having to write a parser for it yourself. And so with systems like BNF or PEG, which Python uses, there are rules that govern how you can define a grammar. And these rules are axioms of those systems. A valid grammar is a theorem of this expression language. These grammars are not inherently useful on their own, but there are tools, parser generators, that interpret these grammars, which yield parsers. The grammar, which is a theorem of an expression language, itself constitutes the axioms of your programming language, which are the rules by which you can construct a program. Now, these programs are meaningless on their own, but we have tools that we can combine with a parser that can interpret our programs. These are compilers or interpreters. And that means that valid programs are the theorems of a formal system that is our programming language. Whether a program is valid or correct are two very different questions. It's easy to tell whether a program is valid just by running it through a parser. Correctness depends on whether your program does what is intended. Now, once you have a program in a form that can be executed, you now have yet another formal system, which is the program itself. Programs are a special type of formal system called a state machine. Each instruction inside a computer program transitions the state of memory within a computer. Those transitions are axioms. The set of transitions that could occur in any run of a a given run of a program are the theorems. An execution of a program takes some inputs, produces some outputs, and these are the valid outputs for the program that you have written. Whether those outputs are correct, though, depends entirely on the interpretation of the problem space. You need to understand the purpose of the program, which is something that you can't encode within a program itself. Whether a program is correct depends on careful interpretation of the behavior of the program under execution. You need domain expertise or at the very least an understanding of what a program is attempting to do before you can determine whether it is correct. Again, interpretation of a formal system can only exist outside of the system itself. I'm just going to take a moment to break. I just had a battery warning. Can somebody give me bring my charger? Okay. So, you may ask yourself, isn't that what test cases are for? But test cases are themselves programs. They're a meaningless statement unless interpreted, which is why we have test runners. Test runners interpret the results of running each test case, but they do not tell you that a test and the code that it exercises is correct. It just tells you whether the test passes. Once again, a valid test suite a USB-C. A valid test suite is only a statement of some facts and not the correctness of those facts. It's again necessary to step outside the system to determine whether it's correct. And so this continues. No matter how low level in the stack we operate, computer programmers do not engage in the truth. We merely deal with transforming expectations into logic and interpreting what follows from that logic. Correctness does not come in to what we do as computer programmers and nor does the truth. Instead, all we do is ensure that we are properly understanding the expectations of the problem space that we're operating in and that the programs we implement meet those expectations and also have the future capacity to meet any expectations that haven't been communicated. Correctness isn't an inherent fact. Correctness is emergent in our understanding of a problem space. Have we built something that's right for what we and our collaborators know? Have we built something that enables us to adapt to changes in circumstances that may emerge in the future? Correctness only ever follows from understanding. And so working entirely within formal systems doesn't give us a useful view of what it is that we do exactly. It gives us precisely no tools to know if what we're doing is of utility or solves the problems that we might be dealing with. We need an entirely different model to reason about what it is that we do. And one model that I find particularly compelling is the theory building view of software engineering. The theory view uh theory theory building view of programming was introduced by Peter Naur, the former formal systems guy, in a presentation in 1984. Naur's thesis, which was 42 years ago now, gives words to a number of things that we've subsequently taken for granted about the way that we build computer programs. And he does this through centering software engineering programming, as he called it, as an activity around the development of knowledge and not, principally at least, around pure output. Naur said, somewhat controversially at the time, that the proper aim of programming is not to produce programs. Instead, it is to build theory about how our problem is solved by having a program there to solve it. Another way to put it is that in addition to having confidence that a problem is solved, you and your team need to build an understanding of how you solved that problem. The assumptions that are made in solving that problem, the allowances that you made for the very definition of the problem to change, and confidence that you and your fellow developers share that understanding. Naur also suggests that documentation is necessarily an auxiliary artifact of any system. This is a modest statement, but extremely cons- consequential. Text, be that natural language or code, cannot communicate all of the intents behind a program. All of the assumptions, large or small, that went into the solution, or of all of the behaviors, potential or observed, a program is likely to encounter. Much knowledge is contextual and comes with experience in thinking about the problem. And so a theory of a program is not the program itself, but the knowledge of the program, which is both explicit in the form of code and documentation, but also implicit. The intents behind certain choices, understanding of how a system behaves under execution, and experience in how the system might behave as certain changes are made. All things you might think of as externalities if you don't pay attention to how development really happens. And Naur goes further to dismiss the idea of computer programs as mere text that can be edited freely. Unlike text, computer programs bear the weight of existing expectations, of retaining behavior in spite of changes, and retaining compatibility where data is concerned. These factors and several more have traditionally tilted the balance between rewrites and modification in favor of modification. The theory building view of programming argues that developers perform best when they anticipate the sorts of modifications that will be made to a system, build with those modifications in mind, and then subsequently implement modifications using those facilities that they built earlier in the development cycle. So Naur argued that modification is the essential part of developing a computer program, and in the decades since we've gained a lot of experience in modifying software. Uh my own take is that codebases only ever change in two ways. Things get edited or things get added. Sometimes, often in fact, unless you're writing a library, a modification is going to consist of both. What I'm going to call accretion is the process by which conceptually new code gets added into a codebase. New modules, new functions, things that didn't exist before the modification was made. Conceptual links tend to form uh not between accreted code and the code there before it, but they're instead reinforced by code that gets added on top. Revision for the purposes of this talk is when you alter an existing model module to account for changing requirements or expectations with regards to a unit of code. What results is a piece of code in the place of an old one with new behaviors. Accretion and revision are two different ways you end up with new behavior in your codebase. With accretion, you end up with two units of code, which may do conceptually similar things, but for different use cases. When you revise, you end up with maybe one piece of code that can handle two use cases. Now, in our current approach to software engineering, accretion has advantages that are felt immediately in the engineering process. If you unit test everything and you revise the behavior of an existing function, you have to ensure that every downstream dependency, or every downstream test, remains functional. Or you have to change those dependencies or re-implement tests to meet the revised assumptions. Revision requires a thorough understanding of the theory of your system and how the revision modifies the existing theory. And that's only for old use cases. You still have to account for the behaviors and the assumptions that you've newly added. Accretion, on the other hand, leads to an increase in the complexity of the given codebase, be that through sheer lines of code or through the number of parts that exist within the codebase. Both of these correspond to less effective maintenance cycles and a higher defect rate. So accretion leads to more immediate productivity by metrics like PRs merged, for example, while revision leads to code that is easier to reason about over the long term and more likely to yield a coherent theory amongst its developers. Revising code gives you the opportunity to revisit the code and the theory that backs it. It can solidify your understanding of how both the original and the modified code performs. These theories of change are in constant tension with each other, and if left unchecked, accretion wins. Uh this is due to a phenomenon that Rommel Gladstad Lefkowitz calls lithification. Once a function stops being modified and is used increasingly as a dependency of other functions, the specific behaviors of that function become depended upon. Put another way, once people start relying on the behavior of a piece of your functionality, you lose the ability to modify that functionality. So to add new behavior, you must accrete code. And this begins a vicious cycle that prevents you from building the theory necessary to keep a project afloat. The one chance you get to revise behavior is early, before you become a widespread dependency. It's impossible to break interfaces once they're published. Ask anyone who's had to maintain a framework or a platform with actual users. If you're wondering why AWS or Azure are so damn complicated, this is why. They have no choice but to accrete functionality. Once you sell an SLA on one piece of functionality, it has to remain there. So in the 1980s, at least some of the people working in software engineering had some idea that theory building was the essential factor in software engineering. >> [snorts] >> Most engineering processes that were built around the delivery of computer programs factor this in. Requirements gathering is a human-oriented process. You talk to people with knowledge of the domain being modeled, and you write requirements that are a good representation of the problems that need to be solved. In the early days, computers were available only to big organizations, who tended to have well-known processes that could afford having requirements gathered and models validated in advance. That's perfect for waterfall. But for basically everything else, that doesn't work, and that's why we have agile methodologies. Take Scrum. It's built around sprints, but the point is not the sprint itself, it's how sprints enable a useful feedback cycle. You have a cadence for sharing prototypes or features with your domain experts, so they can give you feedback, and you can adjust. Velocity of feature delivery increases as you increase alignment between what the development team are doing and what the domain experts expect. And then there's testing. When you write an automated test, you learn things. You learn different things based on when you write the test. You can practice test-driven development and use tests to write a specification that you can verify automatically, or you can write tests afterwards and verify your understanding. In both cases, you're thinking about the problem space twice, once in the implementation, and then once in how the implementation models the domain. Failing test cases are never about correctness. They simply tell you that your interpretation of the domain does not match the implementation. Thinking about the problem space twice reinforces and validates the theory that you hold about your own code. And then there's the matter of being a team. You might practice pair programming. The clear benefit when you're pairing with someone is that a second pair of eyes can spot a number of bugs as they're written, and also help you make decisions. Less obviously, when you pair, both programmers pairing are communicating the theory of a new part of the program to each other as part of the development process. Two people gain knowledge of a new part of a system. Code review does similar things, but less well from a theory development perspective. Asynchronous dialogue after code is written carries less bandwidth than considering a decision in the moment, but you still spend time communicating the theory of the code base between the author and the reviewer. The value to both of these methods is twofold. You reduce a good number of defects, and you get a second person familiar with a new piece of code. Understanding is what gets shared amongst your team. And this goes back to this idea of correctness. Like in software engineering, nothing is correct. Few pieces of software are bug-free, and our engineering processes are built around this. It's not about eliminating defects, it's them to the point that your expected rate and the magnitude of production incidents becomes manageable compared to your incident response resources. Or put another way, can you maintain a supply of effective and happy on-call engineers who can keep your product working acceptably well for your use case? And so, as correctness is not a thing, neither is an objective definition of reliability beyond a system meeting expectations and performing with the this level of availability or consistency or speed that the users actually expect. Nothing [snorts] is good until it's in the hands of users who are using a system that does what they ask it to do. What makes things good is practicing processes that reduce defects in the moment, that build alignment with the expectations of the people we're making things for, and that increase the skill and understanding in the people we work with, so that the chances of causing defects reduces, and the likelihood of building something that meets user expectations the first time increases. There is value in talking about why we do things the way that we do them. Because when we don't examine why we do things, what we end up with is the ritualization of process. Rituals are things that you do because someone a long time ago said that they were important, and people followed them. Often, there might be a good post hoc scientific explanation for them, but there are often people who just perform rituals regardless of whether they're following an evidence-based grounding or not. But all those pieces of process I just talked about are just that. They're processes. They serve a purpose, each of which have a clear line to the theory building view of software engineering. And when you start to ritualize processes that have a strong grounding in what's actually essential to the delivery of software, you stop realizing the value of those processes. Code review in many cases has become so adversarial that there's a documented psychological condition called code review anxiety. If someone fears judgment, criticism, negative evaluation, that's not helping to build an understanding of the code base. And so, if code review is ritualistic, there's no downside to being an to other people in your team. When it serves a purpose around theory building, the goal being to challenge and to reinforce expectations, and then you can build a shared understanding of the theory that underlies a change. Or you could be on a team that practices Scrum ritualistically, where your team organizes around meeting the cadence of a sprint instead of around the validation or feedback cycles with actual end users that uh make Scrum a useful tool that improves product. Instead, you just get reinforcement that completing your sprints doesn't matter, or at least it only matters to the point where you avoid punishment. Either of those things don't build product, they just build demoralization. Or like you could be writing automated tests that could just be tested by a type checker, or don't test useful behaviors of your code. And this lack of building and sharing a theory of why we do things is starting to have serious consequences. Like it's not what do we gain from having a human review our code, it's well, code review is the thing that gates our mergers. It's not what assumptions do we have from our domain that we need to verify for our code to be acceptable, it's let's make CI go green. It's not like what features will get us the most useful feedback in two weeks' time, it's okay, we've done planning, let's burn down our burn down chart. Like these are targets that have nothing to do with quality. It's only of meeting metrics. Without acknowledging the value of these processes, which we perform as humans in a team working to solve a problem that actual people have, these processes go from being a thing that underpins our very ability to deliver the right thing to something that actively impedes it. So, what of the act of writing code? Like for as long as I've been writing software, let alone professionally, it's been possible to opt out of engaging with the theory of a programming language or the theory of a particular library or framework. Like the internet has been full of snippets and bits of code that are just close enough to what people want to do that squishing them into shape isn't too hard. Like for the motivated prototypist, with the internet and with knowledge of how to query a search engine, it's been easy enough to throw together good code. I've been that person. I've been that person countless times. But this is purely incremental work as part of a broader process. I still have to think about the tests that I write. I have to understand the code that I'm proposing well enough to defend a code review, and I have to be confident that my colleagues will be able to support my code if there's an overnight production incident. And of course, that's changing. Like over the last year, we've suddenly hit the point where there are tools that will attempt to automate any task that you ask of it, and superficially, they work pretty well. Like it goes without saying, you can ask an agent to automate the task of researching a library's interface and preparing some code that uses that library to achieve something that looks like the intended result. But also means that you can get agents to write tests for you. You can churn out prototypes of features faster than a product manager can request them. You can get two agents to perform an adversarial code review that will likely find some generic-sort-of-looking bugs. These all move the needle on raw output, but on their own, they don't help users build theory of what a system is for and how it achieves that purpose. And neither do agents do the work to build theory if you leave them to the to their own devices. Uh the ongoing Cooper events study from Stanford shows not only a severe reduction in capability as tasks get more complex, but frequently a significant drop in capability as you attempt to orchestrate them. Indeed, agents can have predictable failure rates, but the spread of these failures is not uniform. The shortcomings do not fully overlap with each other. Without doing work to understand output and recalibrate direction every step of the way, or solve a problem in a completely different way to what's suggested of you, coordination failures magnify each other. And so, what we're feeling now is the pressure of a profession that's been quite ill-defined for a very long time, and industrialized cognitive debt from failing to reckon with that need to define what it is that we do exactly. And consequently, we have huge proportions of the industry who act ritualistically instead of building and reinforcing infrastructure that underpins their team's ability to do their job properly. We don't understand what things are essential or why. And when we don't talk about why parts of our job are essential, there's a strong temptation to treat everything that slows down our raw output as friction. And when you see everything as inessential friction, the natural response is to eliminate it, so you can end up with something that's automated and in many cases entirely not fit for purposes. In that context, coding agents couldn't have come at a worst time. We're experiencing an explosion of tooling which in an ideal sense gives its operator absolute choice in what friction they want to eliminate in their development process. And there's two sides to this. Friction gets in the way of the speed of producing output. Sometimes, friction is essential. We want output to slow down. Sometimes, friction is accidental. For people who have a good understanding of what their system is trying to do, removing accidental friction is a productivity gain. This is why Python is a good thing. Like for anyone, removing essential friction, though, can be catastrophic. Like if time is truly at a premium, and you know what your end state is going to look like, automating the act of researching libraries and making a first pass at code structure is truly removing accidental friction. On the other hand, building even a basic theory of a code base still appears to be essential. If you don't understand how a code base does what it does, or what technical decisions led to things being a certain way, you can't give an agent enough context on a problem that you're facing, and there's a very strong chance that you'll magnify the mismatches between your system's theory and the problem domain that you're modeling. And frequently, the burden of that mismatch falls on people who are already significantly overburdened. Like I don't think it's productive to talk about the output of modern LLMs as inherently being slop, though a lot of it is. But agents can certainly magnify the ability of of people to produce output in the direction that they are pointed at when they prompt their agents, and there's no mechanism to correct that direction once it's been set. So, we're going from a world where all kinds of friction are unavoidable in any development process to one where any developer can opt out of any friction they choose to. We've gone from it not mattering if friction is essential or accidental to one where it absolutely matters. And we haven't done a good job of spreading the theory of why any particular part of our processes are essential. It's probably also the case that essential friction is different from project to project. The act of writing code is not essential to a number of programming tasks. It does not follow that it's inessential in every task, particularly but not exclusively in cases where there's a strong incentive to keep a project compact. Agents are far more effective at accreting code than performing revisions. It's also fairly clear to me that even if some friction turns out to be accidental, this increases the necessity of other parts of our processes. If nobody with accountability is writing code, then that increases the burden on people who have accountability to actually read it. And we've already seen the effects of big organizations that you've probably heard of failing to reckon with the rebalancing of critical points in their processes. If your acceptance processes aren't robust, then increasing the amount of code you output will magnify your defect rate and people will notice. If you don't understand the value of code review and you decide to implement writing and reviewing code as a two-step coordinated automatic process, then automating those two tasks just means you're going to fall victim to the coordination gap. Both the act of deciding that code is adequate, no matter how it's authored, and of reviewing it demands a comprehensive theory of what's going on. For any sufficiently large problem, by the sheer impossibility of communicating the complexity of the spaces we try to model, you're not likely to be able to give a model enough context to make it understand, let alone act on all of that theory. To paraphrase an often misattributed quote, and I'm not advocating configuring your CI while drunk here, adjusting friction in parts of a software development process demands that you adjust your approach to other parts of the process to compensate. And for that, you need to understand the point of anything. When every part of your process is treated as ritual, you don't have a theory for what you're actually adjusting, and you can all too easily end up with something that doesn't result in good product. A striking thing for me is that many people are seeing a deluge of bad practice right now had seen the shape of this bad practice in the past before it started being automated. But because we haven't done the work to understand what it is that we do, this rot of misunderstanding is spreading and it's spreading fast. For everyone who's delighted by previously essential constraints being lifted on their work and doing faster work because of it, there's someone else dealing with a hundred people each imposing their new-found lack of constraint on someone who's not able to deal with it. So, making computer systems is an interpretive exercise because there is no such thing as correct. The burden is on us as humans to know what we're trying to achieve, to build something that starts to achieve that thing, and to verify it. We've had processes in the past that take time, which for the longest time have been constrained by the speed at which we can achieve the tasks that comprise those processes. Until recently, we've had the privilege of enough time to build theory and to communicate it to other people and ensure that we're building the best thing that we can under our constraints. Now we have processes that are being disrupted. We're discovering that friction that we had taken for granted can be removed without immediately discovering the consequences. One conclusion that people are all too happy to jump to is that all friction is inessential. That's not true. We're seeing this play out in organizations who've gone all in on agent-based coding without understanding what they do to everything else in their processes. Understanding what is essential, however, is something that we as an industry didn't work to establish. Testing or sprints or doing structured requirements analysis is for too many organizations an intuitive task. It's not immediately clear that the need to write code yourself isn't also solely justified by intuition, especially for people whose other theory-building processes are not functioning well. But we lack the tools to reason about how our entire process needs to adjust when we choose to adjust just one part of it. And now we're adjusting the one expectation that we least expected that we would need to, and consequently, that's the one we are least prepared to adjust. The value of our profession has never been our ability to produce code that's correct. Software engineering is an interpretive exercise. We interpret a problem space, we use our interpretation to model that problem space in software, and we make modifications as we learn how our interpretation is out of alignment with the reality of the problem domain that we're modeling. Our interpretation and understanding of a system, that stuff that we can't write down, is an externality of the systems that we build. But it's a nece- it's a necessary externality. This is why the processes that we use to get new versions of our systems into production are also ones that increase and reinforce our understanding. Understanding is what helps us get through production incidents when they come up. Understanding is what lets us avoid production incidents in the first place. Understanding is what helps us truly know the difference between a bug or a feature. For many of us, even or especially those of us who aren't changing the way we author our own code, the way the teams around us work is changing at the moment. And so, what I ask of you as you go out into the world is to ask, do you understand how your systems are structured? Do you understand how your systems work? Do you understand how your systems solve problems for the people who use it? What are you doing to build and to keep and to reinforce that understanding? If you don't feel confident in your answer, how are you going to change the way that you work to fix that? No tool in the world can tell you if your system is correct. The only thing we can know for sure is that the work we do serves the people we're building for. >> [applause]