If the dynamics of programs could somehow be made into a topological space then I think good programs would correspond to trivial fiber bundles with simple fibers. The fibers would represent the abstraction layers over the runtime dynamics. In bad programs the fibers would be complicated and less topologically stable, i.e. different abstractions would overlap and there would be no sensible patterns in the fibers.

If this thing existed then static analysis would become a branch of algebraic topology.

I think that wouldn't be a bad place to be a programmer.

In this world one could leverage geometric intuitions to come up with different kinds of program invariants and use the algebra to make it computable. Ya, that definitely would be a nice world to live in.

Now I'm wondering why this isn't a thing already. Why isn't there a formalism for associating more than type information at every point in the program and then trying to reason in a non-trivial way about these associations? This sounds a bit like abstract interpretation and maybe there is something in the literature about combining and reasoning about the combined interpretation.

Sign in to participate in the conversation

Server run by the main developers of the project 🐘 It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!