Simulation as Software: Technical Debt, Epistemic Opacity and Formal Methods

This paper argues that computational models are constructed artifacts as well as representations of reality: objects shaped by methodological choices, technical limitations, code, numerical procedures, and institutional contexts. Assessing the reliability of a simulation therefore requires understanding how it was built, implemented, and used, and not only asking whether its results correspond to empirical data. The paper addresses the problem of computational implementation: how can we know whether a model has been correctly transformed into software, especially when the code is too complex to be fully inspected by a single person? Its central claim is that the means of answering this question already exist and are not being used where they matter. Newman (2016) has shown that much apparently insurmountable opacity comes from poor architectural design and weak software engineering practice rather than from limits inherent in computational science. Good engineering, however, still cannot make a large code surveyable step by step. Formal methods do something different: they shift part of the burden of surveyability to checking procedures that are transparent at the right level of abstraction and whose results different agents and machines can recheck, so that what must be trusted is a small set of explicit commitments rather than an opaque mass of computation. Type systems, proof assistants, and units-of-measure checking have been available for decades, yet they remain largely absent from scientific computing. The paper traces this gap to the technical debt, training, and incentives of scientific software development, and argues that the opacity it produces is a contingent product of practice: an epistemic failure that can be corrected, not a fixed feature of simulation.