There is a folklore correspondence between topology as semi-decidability amongst computer scientists, which is explained in places like:

1. The monograph Synthetic Topology: of Data Types and Classical Spaces
2. An answer by Andrej Bauer on reversing the order of quantifiers .

I recently also learnt that Coarse structures are a type of "dual" to topologies, in that they capture "global" behaviour versus "local" behvaiour that topologies capture. This viewpoint is explained in:

• This answer on MathOverflow to the question "dualizing topology", which writes down the topology axioms using category theory and then dualizes the construction.
• In general, the view appears to be held that Coarse Stuctures is the correct way to dualize a topology to study large-scale phenomena. My understanding is that it was used very effectively by Gromov to study hyperbolic groups by considering quasi-isometry.

So, it is natural to ask, "what is the computational equivalent of a coarse structure"? I was hoping the answer would be something like "co-induction" / "making progress", since topology seems to be about "deciding" things. However, I have no clue how to proceed with such a question. I'd love some insight into this.