Algebraic Topology of Programs

My mind was wandering around the ideas of code, abstractions, and hacking when I made a few connections and stumbled on the “algebraic topology” of programs.

Hacking in software is all about breaking abstraction layers. The hacker modifies the layer below and invalidates assumptions in the layer above. This forced link between the layers by the hacker was not intended and so all further reasoning about the abstraction on the top layer and its relation to the lower layers is invalid. By this analogy unsafe languages do not make any guarantees about separation between the abstraction layers so it should be expected that they are hackable.

Now what if we took all these abstraction layers and viewed them as a global object over the runtime semantics of the program. This global object looks like a fiber bundle where the trivial fiber bundles are the simplest possible programs and their associated abstraction layers. If we actually had this thing then we could use our geometric intuitions to come up with different kinds of geometric invariants and then try to see if our programs satisfied those invariants. Programs in unsafe languages would have complicated topological structure whereas programs in safe languages would satisfy some conditions that would make their global topological structure “more pleasant” geometrically. Then, tools from algebraic topology could be used to compute algebraic invariants that could be used to prove “unhackability” or lack thereof. I don’t know what hacks would correspond to though because maps between fiber bundles would be some kind of program transformation and not “hacking”. Maybe hacks would be global fiber sections with some special property that we didn’t expect to see just from the local structure and is actually a global property the hacker discovered. So program properties are claims about fiber sections.

I’m sure I’m not the first person to think of this and if you squint this really sounds like abstract interpretation couched in analogies about fiber bundles. So maybe the folks that work in abstraction interpretation have figured out a combinator calculus for abstract interpreters and I just haven’t heard about it yet. If this is the case and you know then let me know.