Blog / Opinion essays
Changing the frame: Formal modeling with LLM assistance, Part 1
Frames and formal models today
A wide swathe of technical creative activity, from creating scientific models and engineering designs to writing computer programs to making spreadsheets, is aimed at expressing a model of something precisely enough to be operationalized on a computer. The model, or at least the part of it given algorithmic content, is thus in principle mathematizable. We will think of scientific models, engineering designs, computer programs, and spreadsheets all as kinds of formal models, even if the degree to which they are formalized mathematically varies in the current state of practice.
Any formal model exists within some frame,1 defining the concepts and language within which the model is expressed and the rules to which this expression must conform. A typical frame for scientific modeling might be “a parameterized system of ordinary differential equations,” specific enough to unambiguously describe a class of models and to support uniform algorithms for fitting and simulation. The frame for a computer program is, to a first approximation, the programming language in which it’s written along with the ecosystem of libraries supporting it.
1 We will not attempt to be too precise about what is a “frame”—for us, a pre-theoretical concept—but the choice of word is intended to evoke both a “frame of reference,” meaning a chosen coordinate system or, more abstractly, a chosen point of view, and a “framework,” defined by Wikipedia as an “essential supporting structure on which other things are built.”
Builders and users of computing technology seem to have revealed an overwhelming preference for unconstrained frames.
Frames can be more or less constrained. For example, a paperwork form like a tax return is fairly constrained, prescribing a rigid structure for the requested information, while a survey posing short-answer questions is much less so. A relatively unconstrained frame has the obvious benefit of allowing creator flexibility to formally express their intent. A relatively constrained frame carries a more definite and opinionated viewpoint, stipulating stronger structure and assumptions. This makes it easier to say some things, while prohibiting the expression of other things. That is good when it blocks expressions that would be outright mistakes or, what is more subtle, would deviate from settled design decisions or conventions. It is bad when it prevents useful and desirable expressions not anticipated by the choice of frame.
Builders and users of computing technology seem to have revealed an overwhelming preference for unconstrained frames. From the beginning, the field of computing has, in its theory, emphasized the universality of programming languages; in its practice, language designers herald something more elusive, the “expressivity” of their languages. Meanwhile, the species of mathematized software most widely used by people who are not mathematicians or programmers—the spreadsheet—is highly unconstrained, a blank canvas for tabular data with no further requirements on data layout or typing. Advanced users can introduce their own logic, of arbitrary complexity, within cell formulas, which can vary across cells in arbitrary ways.
It is not hard to imagine what might lie behind this preference for unconstrained frames. Working in a constrained frame, if a creator reaches the boundary of the frame, they may be unable to express their intent at all within the formal model, an experience at best frustrating and at worst intolerable. Think of the anxiety caused by being unsure what to write in your tax return. In the most unconstrained frames, like a general-purpose programming language, it is usually possible to find some way to proceed, even if it involves blurring or subverting what were once crisp abstractions. Put simply, most people would rather muddle through than risk hitting an immovable wall.
Nevertheless, the costs borne under the status quo are severe. With the frame for the formal model having few hard constraints, the typical software project of even moderate complexity relies on a web of semi-formal and informal abstractions described by a mix of code and documentation but not fully specified by either. Rather, the abstractions are maintained—if they are maintained—by a shared understanding among the engineering team, created and renewed through careful communication. Competent programmers create bugs not by trivial logic errors but by failing to understand intricacies of what software abstractions assume or how they interact with each other.
As for spreadsheets, a notorious weakness of the spreadsheet frame is in transitioning from individual use to reliable organizational processes. Because the assumptions behind a spreadsheet are highly implicit, hidden within a web of cell dependencies and in the mind of the spreadsheet’s designer, it is all too easy to make ad hoc changes that silently break those assumptions. The lack of type constraints in spreadsheets is a frequent source of errors, including the perennial joke that Excel interprets every input it sees as a date. In finance and office work, the imperative of reliability has for decades spurred expensive consulting efforts to shift processes from spreadsheets to bespoke software systems—often indecisively, since the replacement systems tend to be less flexible and adaptable for their users.
While different in many respects, what unites the standard paradigms for programming and spreadsheets is that by situating the formal model in a generic and unconstrained frame, the domain-specific abstractions that inevitably support the model possess little formal content; to compensate, disciplined human processes are required to safely use and change the model at any scale beyond a single person.
The effect of emerging LLM technology
The process of creating models forces us to sharpen and clarify our ideas.
Such is the status quo, an equilibrium beset by familiar problems but so far ultimately workable. New technology, in the form of generative machine learning based on LLMs, threatens the status quo by changing the tradeoffs involved. It also presents an opportunity to rethink how we design technologies for formal modeling.
In programming, the emergence of LLMs is decreasing the cost of generating more or less functional code, while exacerbating the challenge of maintaining a coherent set of abstractions and assumptions. The experienced programmer, when attempting to make a change, will notice when the change seems to depart from existing structures or assumptions and take the opportunity to rethink their approach, which can ultimately lead to revising past design decisions or changing the abstractions. The LLM, ever compliant, proceeds along the path of least resistance. More fundamentally, while adept at mirroring surface-level patterns present in the codebase, the LLM is not privy to the web of shared mental representations that enable the effective engineering team to function.2 Thus, at present, LLM coding agents appear to enable significant short-term productivity gains while gradually eroding the codebase’s overall concision and coherence. As LLMs become more prolific in office work, the lack of explicit structure and typing constraints in tools like spreadsheets will only exacerbate the fragility already present. In both cases, the distinction between creating, an active process that engages the mind and forces it to confront problems, and reviewing, a passive activity often experienced as boring, means that opportunities to catch mistakes or revisit assumptions are more likely to be missed when LLMs are heavily involved.
2 The use of Markdown files like AGENTS.md is a primitive means to mitigate this problem.
With LLMs having become so fluent in formal languages, a mainstream view now holds that the problems around sharing formal artifacts between humans and agents are best solved by having humans cease to directly interact with formal models at all. A formal model is useful, the thinking goes, only insofar as it fulfills some externally validatable purpose; if it does so adequately, it does not matter how the model was constructed or how messy it might be internally. The LLM will mediate the interaction between the human and the formal model exclusively through natural language, so that the human never has to look inside.
Whether or not it is technically feasible, this vision misses much of the point of using formal models in the first place. Be they scientific models or computer programs or spreadsheets or abstract philosophical schemes, mathematical (or at least mathematizable) models have been among humanity’s most successful tools to augment our capacity for thinking. Not only does having good formal models increase our powers of deduction, prediction, and counterfactual reasoning, but the process of creating models forces us to sharpen and clarify our ideas, both for ourselves and to communicate with others. To abdicate a direct role in formal modeling would be to weaken human capability and agency.
The question then is not whether we should continue to directly interact with formal models but how the process of model building should adapt to a potent new source of automation and augmentation.
The future of formal modeling
All of the foregoing points to the same conclusion: that safe and reliable formal modeling pairing humans with LLM agents requires more constrained frames than are common today. Under our meaning of “frame,” this entails more than a Markdown file making vague suggestions; a frame specifies concepts, language, and assumptions that set the rules for formal modeling and are enforced when type checking a putative model.
Insist on more constrained frames, while making it possible to change the frame.
How can we adopt more constrained frames while retaining the flexibility that has made the present paradigm of unconstrained modeling dominant? The question may seem paradoxical but the answer is, in a sense, simple: by insisting on more constrained frames, while making it possible to change the frame when needed.
This claim is more easily asserted than realized. Existing languages and tools that serve as frames for formal models tend to be very rigid. Changing them is costly and impractical. There are two reasons to believe that now is the right time to build more malleable tools for formal modeling.
First, as we have seen, LLMs have made it cheaper to generate code and other formal artifacts; consequently, they have made precise specification both more useful as input and more necessary to prevent abstraction drift. There is a growing recognition that existing practices must change. This recognition should create the will to explore new paradigms rather than tinker around the margins of existing ones.
Second, there is now a mature enough body of theoretical knowledge to build the new infrastructure that will allow fluidly defining and changing frames. This body of knowledge is broadly categorical logic, the intersection of category theory with mathematical logic and type theory.
That logic and type theory are the mathematical underpinning for syntax in formal modeling is generally appreciated, and the use of categories as denotational semantics for programming languages is familiar to experts. Much less appreciated, even among experts, is how category theory provides a meta-mathematical toolbox to enable modularity and reuse within and between frames. We refer to specific technical ideas but also to cultural attitudes about how to design formal languages. As we have noted, language designers have overwhelmingly sought to create ever more general and expressive languages, the ideal frame in which to say everything that can be said. This attitude is essentially reductionist. Category theory encourages us to see logic not as something prior to mathematics and science, but as a part of it, and to search for well-adapted mathematical universes in which to create models.3 These universes can look familiar, like functional programming or first-order logic, but can also natively encompass non-standard features crucial to certain domains, such as resource sensitivity, reversibility, temporality, nondeterminism, probability, and fallibility. Categorical logic offers a uniform technical toolbox to describe these paradigms without privileging any of them.
3 The evocative phrase “mathematical universe” we borrow from Ingo Blechschmidt’s paper on exploring “custom-tailored mathematical universes”, where it means a purpose-built topos. For technically minded readers, we remark that our usage is intended to encompass categorical-logical structures generally, not only toposes.
In the CatColab project, we are exploring this vision for scientific and cyberphysical modeling, programming in domain-specific logics, and tabular and relational data. It is beyond the scope of this post to describe these efforts in detail, nor do we claim to have a complete account of any of these vast topics. Rather, in the next post in this series, we will hone in on one of the paradigms highlighted above—spreadsheet-like data modeling—as a case study in how to build tools, underpinned by categorical logic, that set constrained frames for formal modeling while also allowing the frame to be changed fluidly.