The commenter is better served browsing through some introductory formal verification material like Concrete Semantics by one of the same authors as the linked document.
For example, a couple weeks ago I was musing about optimal vertex renumberings so that "the (0/1) adjacency matrix of a non-densely-connected acyclic digraph's transitive closure" scores well according to a domain-specific compressibility metric.
Specifically, at column i and row j is a 1 if and only if (using the post-remumbering indices) vertex i was reachable from vertex j in the original input graph.
The compression results from only storing start and end indices of contiguous runs of 1s in a row. [Edit2: the score of a specific vertex renumbering is the the number of such runs for the complete matrix. Only uninterrupted runs of 1's count.] It is easy to see that a renumbering that results in a triangular matrix won't be terrible, and simple deepest-branch-first depth-first enumeration of the input DAG's undirected "version" (one just ignores edge direction for this step) is at least fairly good for sub-quadratic in vertex count (assuming an average degree much smaller than the number of vertices).
[Edit1: I forgot to point out that this is extremely close to plain run-length-encoding of the matrix in row-major order, except for the fact that RLE cares about a row-crossing run and I don't.]
But exhaustive renumbering testing is O(n!) for n vertices.
I think topology could help me, but I'd need to know some topology to find me way around the literature.
I'll note that I mentioned basic topology in my reply, because topology does indeed have deep connections with type theory that most formal verification systems are based on, interpreting types / theorems are spaces, terms / programs / proofs are continuous functions within them.[1] But basic undergrad topology typically studies more well-behaved (read: more like the real number line) spaces than this.
[1]: https://www.andrew.cmu.edu/user/avigad/Talks/fields_hott.pdf