$\sf HF$-rule: if $\psi(X)$ is a formula in which only symbol $X$ occur free, and in which symbol $X$ never occurs bound; then:
FROM SCHEMA: $for \ i=1,2,3,... \\ \forall X (X \in P_i(\emptyset) \to \psi(X))$
INFER: $\forall X \in V_\omega (\psi(X))$
Where for $i=0,1,2,... \\ \mathcal P_0(\emptyset)=\emptyset \\ \mathcal P_{i+1}(\emptyset)=\mathcal P(\mathcal P_i(\emptyset))$
If we add $\sf HF$-rule to $\sf ZFC$. This would render the resulting theory arithmetically complete! Now any fragment $\mathcal F$of this theory that has a recursively defined set of axioms, among which are all axioms of $\sf ZFC$; that is closed under effective provability (i.e. the usual finite provability of first order logic), would be recursively enumerable, and so $\mathcal F$ would be an effective fragment of this theory.
$\sf ZFC + HF$-rule would prove all upward iterations of 'arithmetical soundness' over $\sf ZFC$, all theories of which are desired to work with, since we think that this is real actually.
I know that $\sf ZFC + HF$-rule is not an effective theory! But we can work within successive effective fragments of it that extend $\sf ZFC$ without being involved with conflicting results, so its consistent to work within this potentially effective milieu.
This has a clear advantage over mere $\sf ZFC$! We can effectively go upwards adding successive tiers of arithmetical soundness, therefore capturing more and more true arithmetical sentences in an effective manner. And arithmetical sentences are the kind of hard mathematical sentences, ones that might find possible application in our finite world. They are the kind of sentences that we don't want to lose!
Question: what's the general point against working in such milieu? I mean from the mathematical point of view? Since I personally never saw the $\sf HF$-rule added to $\sf ZFC$ before?
First of all, the role ZFC plays is as a "default" theory. As you observe, ZFC + HF-rule isn't effective and needs to be approached via hierarchies; but this means that there's no particular "level" which is distinguished. Meanwhile, there's nothing stopping us from proving conditional results over ZFC in the first place (indeed, large cardinals are all about this!) and there isn't a body of results outside logic which do follow from ZFC + iterated soundness but not from ZFC alone.
Besides, adding soundness principles to ZFC changes its flavor in a way I think makes it somewhat less accessible to general mathematicians: it takes much less work to motivate separation and replacement - even to explain why separation doesn't yield replacement! - than it does to explain why ZFC doesn't already prove its own soundness. This is especially noticeable given that ZFC is pretty well justified as a "stopping point" - it takes a few basic ideas about sets and pushes them as far as they can naively be pushed. And it only gets worse when we have to further explain why the HF-rule isn't effective.
So in my opinion, shifting from ZFC to ZFC + HF-rule doesn't really buy us anything that anyone but logicians care about, more-or-less gives up the "default effective theory" game, and results in a less approachable theory as far as general mathematicians are concerned.