My understanding is that no model-dependent theorem of ZFC or its extensions (e.g., ZFC+CH, ZFC+¬CH) provides any insight into the behavior of Turing machines.

My understanding is that no model-dependent theorem of ZFC or its extensions (e.g., ZFC+CH, ZFC+¬CH) provides any insight into the behavior of Turing machines. If our goal is to invent an algorithm that finds better algorithms, then the philosophical angle is irrelevant. For computational purposes, we would only care about new axioms independent of ZFC if they allow us to prove additional Turing machine configurations as non-halting.