For me, the important intuition in this regard is that, for any mathematical theory to be useful, you need to create a process where you can prove properties about its objects in a finite number of steps. You can handle infinite objects (like sets), but at some point you need to define a finite process that produces some knowledge about the object (for example, deciding if a particular word is a member of an infinite grammar).
Working with infinite objects is like using lazy computations in a functional language - you only use as many steps as needed, even if the process does not have a termination step. (I'm not sure to what degree constructive logics handle this intuition - as I said, I don't know much about them).
I've seen that some models exist for mathematical proofs containing infinite steps, but those don't seem to be widespread - and the models are themselves defined through a finite description; so I think even this extreme case validates my intuition that in the end, the mathematician needs to include just a limited number of clauses in their day-to-day work to get something done, even if those clauses are used to describe infinite objects.
Working with infinite objects is like using lazy computations in a functional language - you only use as many steps as needed, even if the process does not have a termination step. (I'm not sure to what degree constructive logics handle this intuition - as I said, I don't know much about them).
I've seen that some models exist for mathematical proofs containing infinite steps, but those don't seem to be widespread - and the models are themselves defined through a finite description; so I think even this extreme case validates my intuition that in the end, the mathematician needs to include just a limited number of clauses in their day-to-day work to get something done, even if those clauses are used to describe infinite objects.