[R0b0t1]

It is and is not really relevant for non-mathematicians. If there is finally an digitization of the system then I suspect programmers will find it useful, but until then, it is useful for exploring mathematics separate from set theory. E.g. instead of picking one or the other for a set theory axiom, choose neither.

Probably applicable to finding complexity proofs as well, and optimization.

I reached, some time ago, the conclusion that you could compare programs for equality and determine if they are equal. This traversal of the graph/type theory representation of the program can be NP hard, but it may also not be, and could save lots of time in fields like automatic differentiation by pruning possible solutions that don't need to be evaluated.

To some surprise I'd found other people mentioning this as well.