Hi Florin,
I am in one sense disposed to Wildberger when it comes to mathematics that is computed or that has a physical meaning. There seems to my mind there are two notions of mathematics with respect to infinity and the continuum. The pure notion, which is the standard approach to mathematics, is in some ways Platonic. I am not particularly anti-Platonic, but the problem I see with Platonism is that it largely has nothing to do with most things you actually want to know. The Platonist type of mathematics, which is embodied by ZF or standard set theory, largely exists on its own, and what is actually calculated in both mathematics and physics is some tiny part of this. I am not really that concerned about the existential aspects of set theory and what might be called Platonism, but I don't think this has what I might call a hard existence. For a thing to have a hard existence it must be computed and there must be a physical way it can be represented. A set, number, function that can't be physiccally represented has a sort of "ghostly" existence at best, and I am not out to exorcize ghosts from mathematics particularly. However, for something to have a hard existence it can't be a ghost, it must have "meat."
The "ghosts" of pure mathematics are useful in some ways, for they allow us to make various arguements so that there "deltas" and "epsilons" that fortunately cancel out and we don't have to actually produce an infinitesimal number in our hands. In that sense these can of course have a utility, but this works only when the system is such that an actual infinity, or infinitesimal, is removed from the answer.
This is in a way not that different from nonlocal hidden variables. Do nonlocal hidden variables exists? Maybe, or for that matter sure; I can arrive at a theory (in fact a vast number of them) of nonlocal hidden variable theory. However, there appears to be a serious obstruction to finding any observable consequence to any hidden variable theory. This obstruction is I think a topological property, and has correspondences in sheaf theory. Classical mechanics is map from the reals to the reals. Quantum mechanics is map from the reals, or really complex or quaterion numbers, to a discrete set of numbers corresponding to eigenvalues. Quantum physics says that we can know all sorts of stuff about those eigenvalues, but we have a very limited contact with the continuum stuff that involves waves and fields. Quantum mechanics then might be telling us much this lesson. Any hidden variable theory is then some set of functions, dynamics and so forth, that tell us how the continuum stuff maps to a discrete set of numbers. An obstruction against this appears to be at least similar to a relationship between mathematics that is "ghostly" and that which has "meat."
I am not an expert on type theory and HOTT, but I have been studying it some. I am not sure about actually using this in physics, but this seems to be a reasonable sort of mathematical foundation for the sort of mathematics that could be relevant to phyhsics in the future. It imposes no notion of infinity, but it treats types as unbounded in their cardinality. There is no fundamental limit to their size, but they must have some sort of index, similar to a homotopy or monodromy, that has to be computed --- it must be inserted into some "register" or "slot." I wrote on this topic because it seemed to be the closest thing that fit the question proposed by FQXI.
I have visited your blog site some, but have not had much time to contribute entries. Maybe I will try to be more diligent on that before long.
Cheers LC