Again, all fair. To simplify, my points are to demonstrate a confounding nuance, simple counterexamples where the arguments don't hold.
> Hypercomputation isn't really a big part of the main thrust of complexity theory
I don't mean to imply that it was, though the results are actually relatively important elsewhere.
> That's not complexity theory, at least not the standard theory, which treats time and space (or circuit size) more abstractly than concrete physics.
More, but not totally abstractly. Steps and cells being vacuous primitives, they're not literally space-time, but within orthodoxy there's absolutely a partial morphism that's implied. That's why they're named like that. You are supposed to have them live close together in your head.
>There are, however, theoretical reversible models, just note that they don't yield different "classic" complexity classes
I know that some don't, but for example quantum models to use your own example, while not technically reversible in the absolute sense, do possess some reversibility capability and do derive different complexity classes.
I think it's very obvious that there should be reversible computational models which yield different complexity classes from the typical ones. To me for a field to qualify as a study on the nature of computation, it should probably be able to design one totally a posteriori, if in a higher order language. Complexity theory might be invoked in such a construction, but it's not the one doing the building. It's one of many in an orchestra.
Here's a question I have, since you do seem pretty well versed on CT. Universal quantification over complexity classes of first-order systems, used anywhere in the abstract?
> Universal quantification over complexity classes of first-order systems, used anywhere in the abstract?
I'm not sure what you mean by "complexity classes of first-order systems" and by "in the abstract".
But it seems like you're asking about the intersection of computational complexity and formal systems, and there's definitely work there. I already mentioned proof complexity, which analyses the number of deduction steps needed to prove something in various formalisms, and there are famous undergrad-level examples, such as TQBF (https://en.wikipedia.org/wiki/True_quantified_Boolean_formul...). But an intersection that is of more interest to me, as I'm interested in software correctness, is that of the model-checking problem.
Now, many people are confused whenever the model checking problem is discussed, because they confuse it with model checkers, which are a set of algorithms intended to solve the problem, but complexity theory is typically interested in the inherent difficulty of answering problems regardless of the algorithm used to do it. So the model checking problem is that of determining whether a formula in some formalism implies another formula, and its inherent complexity exists regardless of whether this question is answered via a formal proof or by some technique involving the logic's semantics. In the context of software verification, the model checking problem is that of determining - by whatever means - whether a program satisfies some non-trivial property.
Philippe Schnoebelen has some papers on the model checking problem in temporal logic (https://lsv.ens-paris-saclay.fr/Publis/PAPERS/PDF/Sch-aiml02..., https://lsv.ens-paris-saclay.fr/Publis/PAPERS/PDF/DLS-jcss-p...). One of his findings that I've found most interesting with regards to programming is that programming languages cannot, in general, make answering the question of whether a program satisfies some property any easier. This result is surprising. The reason is that without a programming language, we could describe a program as a huge state transition graph (this is called a Kripke structure). In that representation, it's been proven that verification is linear in the number of states, i.e. there is no general approach that is faster than brute-force. Now, the size relationship between a program written in a programming language and its Kripke structure is easily exponential or more, so if there were no algorithm that's better, in the worst case, than a brute force of the Kripke structure, then obviously verification is intractable in the size of the program. However, the number of Kripke structures of size N that have a succinct representation in some programming language is far smaller than the total number of Kripke structures of size N. So it could have been the case that analysing programs would have been easier than analysing their Kripke structure (while ignoring their representation in the language). But Schnoebelen proved that this is not the case.
He also proves that program decomposition (and verification of each component separately) cannot, in general, make verification any easier (i.e. the model checking problem isn't FPT in the number of program components).
These results are far more recent than the hopes expressed in the seventies and eighties that we'll be able to prove the correctness of all/most/many programs we write, and indeed, even though the results talk about the worst case, what we've seen in the last few decades is that the power of program verification indeed behaves more like the worst case than something far from it. The gap between the size of programs we can verify and the average size of programs we write has only widened (what saved the day has been the effectiveness of unsound methods, but that's a whole other discussion).