The Shape of the Problem: The Geometric View of Software

Software · Geometry · Topology · Part II

The Shape of the Problem

A deadlock is a hole you cannot walk around. A loop nest is a solid you rotate. The impossibility of distributed consensus is a fact about connected spaces. On the geometric view of software — and on exactly where it stops working.

October 2026 · Part II · How We Know Software Works

This is Part II. Part I — The Cheap End of Rigour argued that there is a ladder of techniques between testing and proof, that the industry silently adopted its cheapest rungs, and that the unclaimed value sits in the middle. That piece treated correctness as something you prove. This one takes the other tradition — older, stranger, and less discussed — which treats it as something you see.

When you solve a maze on paper you do not reason about it symbolically. You look at it, and the dead ends are simply visible. When a chess player says a position feels cramped, they are describing a shape. Mathematicians have always known that half of problem solving is finding the representation in which the answer becomes obvious — the same problem that is a page of algebra in one coordinate system is a glance in another.

The question is whether software has such a representation. The optimistic answer is that it has many, each covering one aspect completely and none covering everything. That is a weaker claim than “software is geometry”, and I think it is the true one. It is also more useful than it sounds, because the aspects that do have a geometry are precisely the aspects that produce the bugs nobody can find.

Two claims, and only one of them is interesting

The weak claim is that pictures help you understand code: diagrams, flame graphs, dependency views, time-travel debuggers. True, useful, and essentially pedagogy. The strong claim is that geometry and topology are the actual mathematics of certain software problems — that there are results proved geometrically which cannot be reached any other way. That claim is also true, and it is much less well known.

Programs are paths, invariants are regions

Start with the framing that everything else rests on. A program's execution is a trajectory through a space whose points are its states. This is not decoration; it is what a model checker literally does. An invariant is a region that trajectory must never leave. A safety violation is a path that escapes it. A liveness violation is a cycle you cannot get out of.

Once you accept that, a great deal of technique turns geometric. “The balance is never negative” is a half-space. “These two counters never differ by more than one” is a diagonal band. Proving an invariant means showing the set of reachable states sits inside a given region — and since you cannot compute the reachable set exactly, you compute a shape that contains it.

That is the whole idea of abstract interpretation,[1] and its central design decision is a choice of shape family. Intervals give you axis-aligned boxes: cheap and blunt. Octagons add diagonal constraints of the form ±x ±y ≤ c, at modest extra cost.[2] Convex polyhedra are precise and expensive. Zonotopes and ellipsoids sit in between and are what you reach for in numerical code. The precision-versus-cost dial that every static analyser exposes is, underneath, a geometric dial: how well can your chosen family of shapes hug the true reachable set?

The reachable set of a program is a shape you cannot compute, so you compute a shape that contains it. An axis-aligned box is cheap but clips the unsafe corner and raises a false alarm. Add diagonal constraints — an octagon — and the approximation hugs the real set closely enough to prove the property. Every static analyser's precision setting is a choice from this family.

This same picture runs all the way out into control theory, where reachability analysis propagates flow pipes forward in time, Lyapunov functions are nested level sets shrinking towards equilibrium, and a barrier certificate is a surface separating the reachable from the forbidden. It is the same idea with continuous dynamics: prove a property by finding a shape.

Concurrency is topology, and this is not a metaphor

Now the part that deserves to be far better known than it is.

Dijkstra, in 1968, drew a picture to explain mutual exclusion.[3] Two processes; put the progress of the first on the horizontal axis and the second on the vertical. Any interleaved execution is then a path from the bottom-left corner to the top-right that only ever moves right or up — you cannot un-execute an instruction. A lock held by both processes over overlapping regions of their code carves out a forbidden rectangle: a set of states that cannot exist, because both processes cannot hold the lock at once.

With one rectangle you have an obstacle, and every path can route around it. With two rectangles arranged the wrong way you get something else entirely: a pocket from which no legal path can escape. That pocket is deadlock. Not a metaphor for deadlock — the actual definition, drawn.

Dijkstra's progress graph. Execution moves only right and up, so the geometry of the forbidden regions decides everything. One shared lock is an obstacle you can walk around. Two locks acquired in opposite orders produce a pocket — shaded — where you can neither go up (the first lock is held) nor right (the second is held). Lock-ordering discipline is, geometrically, the rule that arranges the holes so no pocket exists.

This picture generalises. Three processes give you a cube with forbidden boxes; n processes an n-cube. And it grew into a research field — directed algebraic topology[4] — which studies spaces with a preferred direction of travel. The invariant of interest is not the usual homotopy class of paths but the dihomotopy class: two schedules that can be continuously deformed into one another without crossing a forbidden region are guaranteed to produce the same result. Which is the precise mathematical content of the informal claim that “these interleavings do not need testing separately”.

The theorem that geometry proved and nothing else could

In 1993 Maurice Herlihy and Nir Shavit did something that still looks improbable. They took the question which distributed tasks are solvable without waiting? and turned it into a question about the shape of a simplicial complex.[5] The work won the Gödel Prize in 2004, shared with two independent lines of attack that reached related results.[6]

The construction: build a complex whose vertices are the local states a single process can be in, and whose simplices — edges, triangles, tetrahedra — are the sets of local states that can coexist in one global state. Executing a round of communication does not change the complex arbitrarily; it subdivides it, like refining a mesh. The Asynchronous Computability Theorem then says: a task is solvable without waiting exactly when there is a map from some subdivision of the input complex to the output complex that respects process identity.

Now the payoff. Consider consensus between two asynchronous processes. The input complex is connected — there is a chain of compatible states linking “both proposed 0” to “both proposed 1”. The required output complex is disconnected — the processes must all decide 0, or all decide 1, and nothing in between is permitted. And subdivision followed by a continuous map cannot disconnect a connected space. Consensus is therefore impossible, and the classical FLP impossibility result[7] reappears as a statement about connectivity. Push the same argument into higher dimensions and you get the bounds on k-set agreement, which is where the topology stops being reformulation and starts being the only known route.

Why wait-free consensus is impossible, in one picture. A protocol may refine the space of possible states arbitrarily finely, but refinement cannot tear a connected space apart. The required output space has two components and no middle. Connectedness is preserved; the target is disconnected; therefore no protocol exists.

Consensus is impossible because you cannot disconnect a connected space by deforming it. That is not an analogy for the proof. That is the proof.

Geometry that ships in your compiler

The polyhedral model is the case where all of this stops being beautiful and starts being a build flag.

Take a loop nest. The set of iterations it executes — all the (i, j, k) triples — is exactly the set of integer points inside a convex polyhedron whose faces are the loop bounds. The data dependences between iterations form a cone of directions that must be respected. And now every classical loop transformation — interchange, skewing, tiling, fusion, fission, parallelisation — is an affine map applied to that solid. A transformation is legal precisely when it does not reverse any dependence vector. Finding a good one becomes an integer linear programming problem over a lattice polytope.[8]

A loop nest is a set of integer points inside a convex polyhedron; the bounds are its faces and the data dependences form a cone of directions that must be preserved. Loop interchange, skewing and tiling are affine maps on that solid, and a transformation is legal exactly when it does not reverse a dependence. This is not a metaphor for what a compiler does — it is what LLVM Polly and the MLIR affine dialect literally compute.

LLVM's Polly, GCC's Graphite and MLIR's affine dialect implement this,[9] and the entire tensor-compiler world — Halide, TVM, the kernel generators behind every deep learning framework — reasons in these terms. If you have ever wondered how a compiler picks a tile size for a matrix multiplication, the answer is convex geometry and integer programming over a lattice.

A smaller example in the same spirit, and one almost everybody has used without noticing: cyclomatic complexity. McCabe defined it as E − N + 2P,[10] which is the cycle rank — the first Betti number — of the control-flow graph. The industry's most widely deployed complexity metric is a topological invariant. Very few of the people who report it know that, which is perhaps why so few of them can say what it means.

Types as spaces

Since the mid-2000s there has been a reading of type theory in which the geometry is not applied afterwards but built into the foundations.[11] A type is a space. A term is a point in it. A proof that two terms are equal is a path between those points. A proof that two such proofs are equal is a homotopy between paths. And so on, up an infinite tower that turns out to be exactly the structure of higher groupoids.

Voevodsky's univalence axiom then says something with a direct engineering flavour: equivalent types are equal. If you can exhibit an equivalence between your list-based implementation and your array-based one, every theorem proved about the first transports automatically to the second. That is a formal account of what a refactoring is — not “the tests still pass” but “these two representations are interchangeable, and here is the transport”.

I want to be honest about the maturity here: this is largely still latent as engineering practice. Cubical Agda gives it computational content, Lean's library keeps growing, and the direction is clearly right. But nobody is shipping a payment system on univalence this year.

Proofs you can look at

Category theory's basic move is that “these two routes agree” is a picture. A commuting diagram is a claim you can check by eye and prove by chasing arrows. And once you see it, a whole class of refactorings acquires a single crisp criterion.

Does the diagram commute? Validating then serialising and serialising then validating are the same operation exactly when the square closes. Most refactorings are a claim that some diagram commutes; most refactoring bugs are a square that does not.

The more radical version is string diagrams, where morphisms become boxes and objects become wires, and the axioms of the algebra become topological facts about the picture: sliding a box along a wire is a legitimate proof step.[12] Penrose's tensor notation is the classical instance. The striking modern one is the ZX-calculus for quantum computing,[13] a complete graphical calculus in which you verify circuit equivalences by rewriting diagrams — and which is used inside real quantum circuit optimisers. Girard's geometry of interaction and linear logic's proof nets belong to the same family: proofs as graphs, and computation as graph rewriting, where the bureaucratic redundancy of sequent calculus simply dissolves into the geometry.

Landscapes, and the real dividing line

When you are optimising rather than deriving, the terrain metaphor is largely honest. Loss surfaces, basins of attraction, saddle points, ridges, plateaus — all of these behave enough like landscape to reason about.

But the geometric fact that actually matters in optimisation is convexity. Rockafellar's remark is the one to remember: the great watershed is not between linear and nonlinear, it is between convex and non-convex. If the feasible region is convex, every local optimum is the global one, and that single geometric property is what makes linear and semidefinite programming tractable. When someone tells you a problem is hard, the useful follow-up is rarely “how many variables?” and almost always “is it convex?”

Information geometry takes this one step further and is worth knowing about: probability distributions form a Riemannian manifold under the Fisher metric, and the natural gradient is steepest descent measured in that geometry rather than in whatever arbitrary coordinates you happened to parameterise with. Much of what looks like optimiser folklore is a statement about using the wrong metric.

One more, less glamorous and more immediately profitable: spatial locality is real geometry with real consequences. Cache lines, page boundaries, struct-of-arrays against array-of-structs, and space-filling curves — Morton order, Hilbert curves — used to flatten multidimensional data into one dimension while preserving proximity. Data-oriented design is, at bottom, the argument that you should think about the shape of memory before the shape of your class hierarchy.

The shape of a codebase

At the architectural level the geometry is graph-theoretic, and this is the part you can act on this week.

View	What it is	What it tells you
Dependency graph	Modules as nodes, imports as edges	Cycles — the module-level equivalent of a knot. Every cycle is a decision you deferred.
Design structure matrix	The adjacency matrix, reordered so clusters sit on the diagonal	Everything off the diagonal is coupling. Modularity becomes visible as block structure.[14]
Spectral clustering	Community detection on the dependency graph	What your modules actually are, as opposed to what the directory layout claims.
Change coupling	Files that change together, mined from git history	The empirical architecture. Where it disagrees with the structural one, your architecture is lying to you.[15]

The last row is the one I would run first. It costs an afternoon, it uses data you already have, and the divergence between the graph your code declares and the graph your commits reveal is as good a map of technical debt as anything you can buy.

Brooks's objection, which is correct

Any argument of this shape has to answer Fred Brooks, because he made the counter-case well enough that it has never really been refuted. In “No Silver Bullet” he listed invisibility among the four essential difficulties of software.[16] His claim: software has no natural geometric embedding. A floor plan is a complete description of a building because buildings are three-dimensional objects. Software's structure is a superposition of several distinct graphs — control flow, data flow, dependency, name scope, ownership, temporal behaviour — which are typically non-planar and which do not share a layout. Any single diagram is a projection that throws most of it away.

That is right as stated, and it is usually over-generalised. It is an argument against the existence of one master picture. It is not an argument against the local geometries above, each of which is a complete and faithful description of one aspect. The lesson to take is that you should expect a family of projections rather than a blueprint, and that choosing which projection to look at is itself a skill.

The second caution: intuition breaks in high dimensions

Almost all the volume of a high-dimensional ball sits near its surface. Random vectors are nearly orthogonal. The corners of a hypercube dominate everything, and there are exponentially many of them. Distances concentrate until nearest and farthest neighbours become nearly indistinguishable. Reasoning about a two-hundred-dimensional configuration space using three-dimensional intuition will mislead you, and it will mislead you confidently. Geometry is a tool here, not a licence.

What to do with this on Monday

Draw the state machine. Most impossible bugs are states you did not know existed. Enumerating them on paper is the cheapest formal method there is, and it converts directly into the model of Part I's fourth rung when you want more.

Use progress-graph thinking for locks. Two axes and a couple of rectangles is enough to see most deadlocks before you write them, and it explains why lock ordering works rather than asking you to memorise that it does.

Plot the change coupling of your repository against its intended module structure. The divergence is the map.

Ask whether the diagram commutes when you refactor. It is a surprisingly sharp test for whether an equivalence you are assuming actually holds.

Think of a type as a space — how big is it, what does it exclude — rather than as an annotation. It is the fastest route to Part I's first rung.

Learn the polyhedral view if you ever touch loop optimisation or tensor kernels. It is the difference between guessing tile sizes and knowing which transformations are legal.

So: is there a more geometric way to think about software? Yes, and in a handful of places it is not an aid to thought but the thing itself — the topology of a simplicial complex settles what a distributed system can compute, and no amount of case analysis will get you there. Elsewhere it is a productive metaphor, which is still worth having. Brooks was right that there is no blueprint. He was wrong to conclude that there is no geometry, and the gap between those two claims is where the interesting work has been happening for thirty years.

If you liked this, read next

Herlihy, Kozlov and Rajsbaum, Distributed Computing Through Combinatorial Topology, for the strong claim in full. Daniel Jackson's Software Abstractions for the practical middle. Bret Victor's essays for the weak claim done properly. And Brooks, still, for the objection.

References

1. Cousot, P. & Cousot, R. (1977). “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints.” POPL 1977.
2. Miné, A. (2006). “The Octagon Abstract Domain.” Higher-Order and Symbolic Computation 19(1), 31–100.
3. Dijkstra, E. W. (1968). “Cooperating Sequential Processes.” In F. Genuys (ed.), Programming Languages, Academic Press. The origin of the progress graph.
4. Fajstrup, L., Goubault, E., Haucourt, E., Mimram, S. & Raussen, M. (2016). Directed Algebraic Topology and Concurrency. Springer.
5. Herlihy, M. & Shavit, N. (1999). “The Topological Structure of Asynchronous Computability.” Journal of the ACM 46(6), 858–923. Gödel Prize 2004. dl.acm.org
6. Saks, M. & Zaharoglou, F. (2000). “Wait-Free k-Set Agreement Is Impossible: The Topology of Public Knowledge.” SIAM Journal on Computing 29(5); and Borowsky, E. & Gafni, E. (1993), STOC 1993.
7. Fischer, M., Lynch, N. & Paterson, M. (1985). “Impossibility of Distributed Consensus with One Faulty Process.” Journal of the ACM 32(2), 374–382.
8. Feautrier, P. (1992). “Some Efficient Solutions to the Affine Scheduling Problem.” International Journal of Parallel Programming 21(5–6).
9. Grosser, T., Grösslinger, A. & Lengauer, C. (2012). “Polly — Performing Polyhedral Optimizations on a Low-Level Intermediate Representation.” Parallel Processing Letters 22(4).
10. McCabe, T. (1976). “A Complexity Measure.” IEEE Transactions on Software Engineering SE-2(4), 308–320.
11. The Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. homotopytypetheory.org
12. Selinger, P. (2010). “A Survey of Graphical Languages for Monoidal Categories.” In New Structures for Physics, Springer Lecture Notes in Physics 813.
13. Coecke, B. & Duncan, R. (2011). “Interacting Quantum Observables: Categorical Algebra and Diagrammatics.” New Journal of Physics 13, 043016.
14. Baldwin, C. & Clark, K. (2000). Design Rules, Volume 1: The Power of Modularity. MIT Press.
15. Tornhill, A. (2015). Your Code as a Crime Scene. Pragmatic Bookshelf.
16. Brooks, F. P. (1987). “No Silver Bullet — Essence and Accidents of Software Engineering.” IEEE Computer 20(4), 10–19.

Published October 2026 · Part II of How We Know Software Works · Part I: The Cheap End of Rigour.

On method and tools

This piece was written collaboratively with Claude Opus 5 (Anthropic): human specification and critical review, machine synthesis and drafting. The diagrams are schematic rather than to scale — the progress graph and the abstract-domain figure illustrate the mechanism, not a particular program. Where the geometric reading is genuinely the mathematics (the Asynchronous Computability Theorem, the polyhedral model, cyclomatic complexity as a Betti number) that is stated as fact and cited; where it is a useful metaphor (landscapes, the shape of a codebase) it is labelled as one. Brooks's objection is included because it is the strongest argument against the piece's own thesis.

The hardest thing about a geometric argument is knowing when the picture stopped being the thing and started being a picture of it.

Authored by: Luis Matos Ferreira
Physicist & Developer