Where do correctness and understanding live in research software?
Charity Majors believes it’s a “when” and not an “if” that we ship code we have never looked at to production, and on the Pragmatic Engineer podcast she describes code going from “pets” to “cattle” (Orosz 2026). It’s the analogy from infrastructure in the 2010s: a pet server is set up by hand and nursed back to health when it gets sick, while cattle are identical and simply replaced. Part of how she got there is Chad Fowler’s Phoenix Architecture, where “Tests and evaluations define truth, not files.” (Fowler 2025)
To be fair to her, she doesn’t say understanding doesn’t matter. She says it has to move out of the code: “Code becomes precious when it is the only place knowledge lives,” and “The knowledge in our heads is unavailable to AI until we encode it into the system.” (Majors 2026) That is, into specifications, tests, evals and observability. For product engineering, I think this is plausible.
But these two points unsettle me when I think about scientific computing. If she’s right, and it applies to us too, “shipping unread code” almost by definition means we have no understanding, and “truth lives in tests” seems opposite to what correct should mean in science. So how much of what software engineers are learning about agentic engineering carries over to research software, and to simulation and scientific computing code in particular?
At the other extreme is Peter Naur, for whom the program is the theory in its programmers’ heads, and the documentation can never hold it (Naur 1985). I’m looking for somewhere in between, more practical for scientific computing.
Where correctness lives in scientific computing
What we want to be correct is a chain:
- The mathematics you want to compute: the model equations.
- The approximation: finite grid, finite differences, truncation, etc.
- The algorithm: ideally the same as the equations you wrote down, but it can hide more bugs.
- The code.
Tests only reach the last link, and only at sample points.
In places, scientific computing actually has better verifiable signals than product code: the method of manufactured solutions (Roache 2002; Salari and Knupp 2000), the observed order of convergence under grid refinement, conservation laws and other invariants. So we are not short of verifiers. What they can’t hold is the theory: why this discretization, which invariants it preserves, where the approximation breaks down. And the correctness argument itself is mathematics, not a test.1
The verification and validation (V&V) literature already separates the two: verification is “solving the equations right”, and validation is “solving the right equations” (Roache 1998). I should say I don’t know much about V&V, but I suppose it is the closest thing we have to establishing correctness in scientific computing, i.e. running a simulation built on science to predict something.
One observable universe
In CMB data analysis, it sounds like validation is hard, because we can’t perform experiments. LiteBIRD, one of the CMB experiments I’ve been involved in (along with POLARBEAR and the Simons Observatory), is a space-based experiment, and there is a lot of V&V in designing the sensors and making sure they meet requirements. That was not my part of the job. I was on the simulation team forecasting systematics. CMB experiments in general run a lot of simulations that try to mimic the physical experiment, such as how it scans the sky, to predict the statistical uncertainty it might have, and use those simulations to tell us what the error bars on the resulting measurements are.
But we only have a single observable universe. We can’t really measure the curvature of the universe directly, for example, so I’m not entirely sure what we did would be regarded as validation in the V&V sense. Certainly we have a lot of different ways to convince ourselves we’re doing the correct thing, using indirect probes. To name two famous examples: Planck used the CMB to measure the speed of the Earth. Our motion aberrates and modulates the temperature fluctuations, and from that Planck measured \(384 \pm 78\,\mathrm{km/s}\) (stat.) in the known dipole direction, against \(369\,\mathrm{km/s}\) from the dipole itself. The paper is titled “Eppur si muove” (Planck Collaboration 2014). And given the temperature power spectrum (TT), Planck predicted what the polarization spectra (TE and EE) should look like, and “the data points track the fluctuations expected from the TT spectra” (Planck Collaboration 2016). I first heard about this in a talk by Martin White. We (CMB physicists in general) also compare with how very different experiments would conclude, say large-scale structure and its inference on the Hubble constant.
Still not a Lean proof
Even so, the kind of correctness we bake into a scientific program is not as watertight as a Lean proof. The Navier–Stokes incident is the extreme case: a complete specification as a Lean theorem, a machine-checked proof, and still no understanding. That’s the upper bound on what a correctness harness can do for us, and in research software the harness is never that complete. As I argued in Long-horizon agents write dead programs, we kind of have a fix for correctness, and understanding is what’s missing. If we have even less correctness assurance, we need more understanding.
Born dead
And that’s a bigger problem, because in scientific computing, programs often become dead in the Naur sense. For Naur, a program dies when the team holding its theory is dissolved (Naur 1985). There’s often no stable person maintaining the same piece of software: grad students and postdocs come and go, collaborating and passing it on to other people, and grants come in to hire someone. This is a major problem for RSEs working on projects where cost recovery models drive them to hop on a different project after one finishes.
That’s why Naur’s dead program makes me so uneasy. A colleague and I, both RSEs, worked for more than a year with Daniel Kattnig and his students and postdocs on the Avian Compass, an upcoming open source Julia package of quantum simulations predicting how birds sense Earth’s magnetic field. The two of us designed the program, with occasional meetings with the PI, and then we handed it over and never touched it again. As soon as we delivered it, it was born dead.
Naur vs Majors and Fowler
Naur preferred discarding a dead program over reviving it: “the existing program text should be discarded and the new-formed programmer team should be given the opportunity to solve the given problem afresh”, because “program revival, that is reestablishing the theory of a program merely from the documentation, is strictly impossible.” (Naur 1985)
That sounds like cattle. The difference is that Naur’s rewrite is done by a team that builds a theory while rewriting. Code regenerated by an agent is born dead again. Cattle only works if the whole theory lives in the spec and the validators, which is what Majors means by encoding the knowledge in our heads into the system.
But I don’t entirely agree with Naur’s “strictly impossible” either, at least for scientific software. I can imagine it’s true for complex product software, say, Word. But for scientific software, the theory of the program is, in large part, the theory of physics. The expected knowledge of physics is doing a lot of heavy lifting in rebuilding the theory: why are they doing this approximation? It must be X, Y, and Z. Someone with a common understanding of physics can fill in the blank. So how much of the theory can be rebuilt depends on how much of it the reader already has, and on how complex the program is. I’ll come back to this in a future post about complexity.
Also, why can’t the theory be rebuilt from documentation? If teaching can transfer a theory from one mind to another, and documentation is a form of teaching, why not? Naur’s answer is that reading is the wrong kind of teaching. A new programmer needs “the opportunity to work in close contact with the programmers who already possess the theory”, as in playing a musical instrument, where “The most important educational activity is the student’s doing the relevant things under suitable supervision and guidance.” (Naur 1985) Perhaps that’s why physics helps so much: physicists have already had years of doing under supervision, in physics. And was Naur thinking of a kind of documentation we have since surpassed? Diátaxis has a whole kind of documentation, explanation, that is “understanding-oriented” and should “explain why things are so”. Why can’t we, in principle, and for some in practice, teach the theory of the software in documentation as well?
Literate programming
This is why I keep coming back to Knuth’s literate programming, which I’ve quoted before: “let us concentrate rather on explaining to human beings what we want a computer to do.” (Knuth 1984) It never became mainstream, even after Knuth promoted the idea over 40 years ago. If our standard for a program were the same as for publishing a paper, which is much closer to delivering an understanding, then we’d be delivering a program with correctness together with understanding.
So where would I draw the line between research software you can ship unread, because the tests hold its correctness, and research software you can’t? I think it is the same vague line I mentioned in After Math, and scientific computing is on the side you can’t. If Majors is right on those two points, that may be fine for a product (even research software that’s a product, e.g. a web app visualizing some data), but for scientific computing, shipping unread code means shipping something no one understands, and truth can’t live in the tests alone. I don’t have a sharper line than that yet.
References
Footnotes
For example, by the Lax equivalence theorem, a consistent scheme for a well-posed linear problem converges if and only if it is stable (Lax and Richtmyer 1956). Convergence is what we want, and it is proved about the scheme on paper before any code is written.↩︎