Preparatory Rant

I've gotta tell you, I don't see how talking about "proofs" of the CT or ECT adds any light to this discussion. Such "proofs" tend to be exactly as good as the assumptions they rest on---in other words, as what they take words like "computation" or "efficient computation" to mean. So then why not proceed right away to a discussion of the assumptions, and dispense with the word "proof"?

That much was clear already with the original CT, but it's even clearer with ECT---since not only is the ECT "philosophically unprovable," but today it's widely believed to be false! To me, quantum computing is the huge, glaring counterexample that ought to be the starting point for any modern discussion about the ECT, not something shunted off to the side. Yet the paper by Dershowitz and Falkovich doesn't even touch on QC until the last paragraph:

The above result does not cover large-scale parallel computation, such as quantum computation, as it posits that there is a fixed bound on the degree of parallelism, with the number of critical terms fixed by the algorithm. The question of relatively [sic] complexity of parallel models will be pursued in the near future.

I found the above highly misleading: QC is not a "parallel model" in any conventional sense. In quantum mechanics, there's no direct communication between the "parallel processes"---only interference of amplitudes---but it's also easy to generate an exponential number of "parallel processes." (Indeed, one could think of every physical system in the universe as doing so as we speak!) In any case, whatever you think about the interpretation of quantum mechanics (or even its truth or falsehood), it's clear that it requires a separate discussion!

Now, on to your (interesting) questions!

No, I don't know of any convincing counterexample to the ECT other than quantum computing. In other words, if quantum mechanics had been false (in a way that still kept the universe more "digital" than "analog" at the Planck scale---see below), then the ECT as I understand it still wouldn't be "provable" (since it would still depend on empirical facts about what's efficiently computable in the physical world), but it would be a good working hypothesis.

Randomization probably doesn't challenge the ECT as it's conventionally understood, because of the strong evidence today that P=BPP. (Though note that, if you're interested in settings other than language decision problems---for example, relational problems, decision trees, or communication complexity---then randomization provably can make a huge difference. And those settings are perfectly reasonable ones to talk about; they're just not the ones people typically have in mind when they discuss the ECT.)

The other class of "counterexamples" to the ECT that's often brought up involves analog or "hyper" computing. My own view is that, on our best current understanding of physics, analog computing and hypercomputing cannot scale, and the reason why they can't, ironically, is quantum mechanics! In particular, while we don't yet have a quantum theory of gravity, what's known today suggests that there are fundamental obstacles to running more than about 10⁴³ computation steps per second, or resolving distances smaller than about 10^-33 cm.

Finally, if you want to assume out of discussion anything that might be a plausible or interesting challenge to the ECT, and only allow serial, discrete, deterministic computation, then I agree with Dershowitz and Falkovich that the ECT holds! :-) But even there, it's hard to imagine a "formal proof" increasing my confidence in that statement -- the real issue, again, is just what we take words like "serial", "discrete", and "deterministic" to mean.

As for your last question:

Quantum computing would be a likely counterexample, if in fact it can be instantiated, but are there possibilities "weaker" than quantum that would be counterexamples as well?

Today, there are lots of interesting examples of physical systems that seem able to implement some of quantum computing, but not all of it (yielding complexity classes that might be intermediate between BPP and BQP). Furthermore, many of these systems might be easier to realize than a full universal QC. See for example this paper ^[1] by Bremner, Jozsa, and Shepherd, or this one ^[2] by Arkhipov and myself.

This answer is intended as a supplement to Scott Aaronson's answer (with which I mainly agree).

From an engineering perspective, it is striking that the Dershowitz/Falkovich article uses the word "random" only in the sense of "random-access memory", and moreover, the article does not use the word "sample" (or any of its variants) at all. Rather, the focus of the Dershowitz/Falkovic analysis is exclusively restricted to the computation of numeric functions.

This limitation is striking because the great majority of modern STEM computational resources (I will venture to say) do not respect the restriction to numeric functions, but rather are devoted to generate samples from distributions (e.g., molecular dynamics, turbulent fluid flow, fracture propagation, noisy spin systems both classical and quantum, waves propagating through random media, etc.).

Thus, if the "Extended Church-Turing Thesis" (ECT) is to have substantial relevance to STEM calculations defined broadly, perhaps the exclusive restriction to numeric functions ought to be lifted, and a generalized statement of the ECT be given, that encompasses sampling computations (and their validation and verification).

Would this generalized-to-sampling version of the ECT still fall within the purview of TCS as traditionally conceived? The answer seemingly is "yes", per the TCS Stack Exchange FAQ ^[1]:

We refer you to the description of ACM Special Interest Group on Algorithms and Computation Theory (SIGACT) ... TCS covers a wide variety of topics including probabilistic computation ... Work in this field [TCS] is often distinguished by its emphasis on mathematical technique and rigor.

First of all, contrary to some sources, I claim that the $\text{ECTT}$ can absolutely be understood as a mathematical axiom, or at least as a mathematical proposition if we doubt its truth. Introduce into our working language a new predicate symbol defined on models of computation with the intended meaning that a model is reasonable. This is essentially the same situation Peano and others faced: we already have an intended meaning for the symbols $\{0,1,+,\times\}$, even prior to writing the axioms involving them. At least until we axiomatize it, our theory remains sound under the interpretation of the new symbol, whatever it means, because the only facts about it that we can prove are tautologies. What is reasonable is reasonable, for example. Now add an axiom, the $\text{ECTT}$, which says that this predicate of reasonableness is satisfied by exactly those models that have a polynomial time-translation to a Turing machine. As an axiom it's not falsifiable in the sense of our theory being able to contradict it, as long as the theory was consistent to begin with, but the soundness of our theory is falsifiable: conceivably there is a reasonable model of computation that's not related to Turing machines by a polynomial time-translation. Allowing that this hypothetical discovery might involve a shift in thinking about what is reasonable, that is how I see the formal side. It seems trivial in retrospect but I think it's an important point to delineate the mathematics from everything else.

Overall, I view the $\text{ECTT}$ as a solid principle and axiom. But we have working computers that are well-described by $\text{BPP}$, and there are problems like prime-finding and polynomial identity-testing that are not known to be in $\text{P}$, so why doesn't this violate the $\text{ECTT}$? It doesn't until we can actually prove $\text{P} \neq \text{BPP}$: in the meantime, instead of shifting our focus to $\text{BPP}$, we're no worse off keeping the $\text{ECTT}$ as-is and saying what-if polynomial identity-testing is actually in $\text{P}$. This approach also lets us isolate particular problems we are interested in such as factoring. It's a subtly different assumption than equipping our model with an oracle, since we don't actually change the model, but the effect is the same. From this utilitarian point of view, the $\text{ECTT}$ is sufficient until we can prove any separations. The situation is the same for quantum computing, except we have to build a working quantum computer and prove $\text{P} \neq \text{BQP}$ to really take the wind out of the $\text{ECTT}$. If we just build one without the proof, maybe the universe is a simulation running on a classical computer and the $\text{ECTT}$ still holds, or if we prove it without building one, maybe it's not really a reasonable model. To make the argument really tight, we need problems that are complete for $\text{BPP}$ and $\text{BQP}$ with respect to $\text{P}$, but we can make do with choosing whatever problems we know how to solve.

For example, suppose I claim to have built a machine that factors numbers and that its runtime satisfies a particular polynomial bound. The machine is in a box, you feed in the number written on a paper tape, and it prints out the factors. There is no doubt that it works, since I've used it to win the RSA challenges, confiscate cryptocurrency, factor large numbers of your choice, etc. What's in the box? Is it some amazing new type of computer, or is it an ordinary computer running some amazing new type of software?

By assuming the $\text{ECTT}$, we're saying it must be software, or at least that the same task could be accomplished by software. And until we can open the box by proving complexity class separations, no generality is lost under this assumption. That's because even if the operation of the machine is explained well by some reasonable non-classical or non-deterministic model and not explained by the classical deterministic one we would still need to prove those models are actually different in order to break our interpretation of the $\text{ECTT}$ and make our theory unsound.

To challenge the $\text{ECTT}$ from an entirely extra-mathematical direction, it seems that we'll need a machine or at least a plausible physical principle for solving an $\text{EXPTIME}$-complete problem in polynomial time. Even a time machine implementing $\text{P}_\text{CTC} = \text{PSPACE}$ is not powerful enough to defeat the $\text{ECTT}$ without a proof of $\text{P} \neq \text{PSPACE}$, although it might help us produce one.

To illustrate, Doctor Who has strung his telephone wires through a wormhole and built a contraption that he uses to discover a gigabyte-long formal proof of $\text{P} \neq \text{NP}$. He wins the Millenium Prize, and he has also invalidated the $\text{ECTT}$, because the result implies $\text{P} \neq \text{P}_\text{CTC}$. If his contraption finds a proof of $\text{P} = \text{NP}$ instead, or a proof of the Riemann hypothesis, he still wins the Prize, but that's it — no $\text{ECTT}$ violation. However, the Doctor's contraption seems like a better tool for attacking the $\text{ECTT}$ than my amazing factoring box, since I don't know how being able to magically factor numbers in polynomial time can help me prove that it isn't possible to do the same thing without magic. To be on equal footing it would have to be the case that factoring is $\text{NP}$-complete and also that I (somehow) know a reduction to it from $\text{3SAT}$ — then I could encode the search for a proof that factoring is not in $\text{P}$ as a series of factoring problems and have a chance at finding it before the wormhole reopens.

In the other corner towers Deep Blue, a giant robot designed by a corporation to solve $\text{EXPTIME}$-complete problems. Its challenge is to play perfect chess quickly on all board sizes and convince us all that it can really do that with an unlimited marketing budget. But it doesn't have to justify the uniqueness of its methods to make us rewrite the $\text{ECTT}$, since we already know that $\text{EXPTIME} \neq \text{P}$. This is more trivial than it may appear: if the robot is reasonably constructed, and what the robot does is amazing, then the reasonable model describing it is capable of amazing things and we can repurpose the $\text{ECTT}$ to polish its gears.

In my view, Scott Aaronson's answer is mathematically incoherent, because it's not compatible with any formalization of the $\text{ECTT}$ that I can identify. We are supposed to weigh evidence for and against $\text{P} = \text{BPP}$, but I think we should demand proof not just evidence before we drop the whole idea of the $\text{ECTT}$ or modify it for no practical benefit (nevermind the nasty business of extending the concept of time-translations to non-deterministic models). And as I've argued above the discussion of whether or not quantum computing is real is a red herring without a proof of $\text{P} \neq \text{BQP}$.

Here is a summary of the situation. For any given model of computation, it is inconsistent to simultaneously believe these three statements: the $\text{ECTT}$; that the model is reasonable or physically possible; and that the model is more powerful than a Turing machine. Only the last statement is in the language of our original theory, $\{\in\}$. If it's not already settled, then we're taking a gamble with consistency by assuming it as an axiom, or by assuming the first two statements together which imply its negation. So our only choice to incorporate any of these ideas which is sure to preserve consistency is between a definition of what reasonable means, and a statement that this particular model is reasonable (which by itself, without the definition, doesn't give us much to work with). Of course, we can have both and still be consistent if we change the $\text{ECTT}$ to something else, but this will have been wasted effort if the class separation is settled opposite the way we expected. Regardless, by axiomatizing our reasonability predicate symbol under such a nebulous interpretation, we're taking a gamble with soundness. Before, with our language equal to $\{\in\}$, we only had arithmetical soundness to worry about, and now we are expected to agree about what is reasonable as well.

Having browsed the linked paper by Dershowitz and Falkovich, I believe that its authors also hold an incoherent or maybe just tautological view of the $\text{ECTT}$.