If there is an Arthur-Merlin protocol for knottedness similar to the [GMW85] and [GS86] Arthur-Merlin protocols for Graph Non Isomorphism, then I believe such a cryptocurrency proof-of-work could be designed, wherein each proof-of-work shows that two knots are not likely to be equivalent/isotopic.
In more detail, as is well known in the Graph Non ...
The ideas the question expresses are interesting but maybe insufficiently
fleshed out. I can see a couple of points that deserve further
It is difficult to "code the exact same functionality". In part that
is because what counts as "the exact same functionality" depends on
the chosen notion of program equivalence. For terminating programs
Papadimitriou showed that a version of this problem is PPAD-complete in the paper introducing that class, "On the complexity of the parity argument and other inefficient proofs of existence".
His formulation of the problem is:
Borsuk-Ulam. Given an integer n and a Turing machine computing for each
point $P=(x_1,\dots,x_d)$ with $-n\leq x_i\leq n$ and $\...
Some recent references here from Algebraic Topology, and UGC hardness- Morse Theory , and another reference Unique Games Conjecture and Computational Topology . The latter is about covering spaces of graphs, and "lifting" of graphs, and could point to a deeper link between Topology, and the Unique Games Conjecture.
In Slide 26, Martin Escardo provides an algorithm that might give you what you're looking for:
Go the library.
Pick a book on topology.
Pick a theorem.
Apply the dictionary.
Get a theorem in computation.
See also this paper
How is the oracle given and what do we know about $g$?
If the oracle is black-box and we only know that $g$ is continuous odd, then already for $n=1$ we might require infinitely many questions...
If the oracle is given by some Turing-machine, then you get that your problem is
where the size of the input is length of $\epsilon$...
here is a project Rosetta Code somewhat similar or adaptable to some of your goals [which as others point out are not very specific/objective/concise/clearcut yet], a database involving quantification of languages on the same task for comparison. the post "Code Length Measured in 14 Languages" is an example of the quantitative analysis possible with this ...
Two big applications of homotopy theory in theoretical computer science are
Homotopy Type Theory revealed a completely unexpected connection between the theory of the typed lambda calculus and homotopy theory. As a quick intuition, think of it as either a (vast) generalization of the connection between intuitionistic logic and topological spaces, or a ...
You may want to look at nowhere dense graphs.
One of the reasons why minor-closedness is natural is the following. We typically want to work with families of graphs rather than specific graphs. And we want to solve problems with arbitrary weights/capacities on edges/nodes. Suppose we want to ...
As someone somewhat familiar with termination analysis, I'd say that the techniques are only as ad-hoc as the programs they aim to prove termination of, which is to say very ad-hoc indeed.
The crucial approach to scaling such analyses is modularity which allows decomposing the problem into sub-problems. Indeed this usually consists in identifying cycle-like ...
My answer to a related post: Applications for set theory, ordinal theory, infinite combinatorics and general topology in computer science?:
The 2004 Gödel Prize was shared by the following two papers:
The Topological Structure of Asynchronous Computation.
By Maurice Herlihy and Nir Shavit, Journal of the ACM, Vol. 46 (1999), 858-923
Wait-Free k-Set ...
the Rosetta Code repository has been used for a new comprehensive scientific/ academic study of language succinctness among other comparisons of properties. announced at "Analyzing Programming Languages using Rosetta Code"
A Comparative Study of Programming Languages in Rosetta Code Nanz/ Furia
Sometimes debates on programming languages are more ...