The axiom system PRA of "primitive-recursive arithmetic" is finitistic, but it has been known for a few decades that it has the same set of $\Pi^0_1$ consequences as the infinitistic theory $\text{WKL}_0$ of second-order arithmetic. In particular, there is a primitive recursive function $f$ that turns a formal proof of a $\Pi^0_1$ statement in $\text{WKL}_0$ into a proof in PRA. Roughly put, a $\Pi^0_1$ formula says that all natural numbers have some particular property, depending on the formula, where the property can be stated using a formula in the language of rings with no quantifiers. 

The advantage of working in $\text{WKL}_0$ is that the proofs can be much shorter. I think this was always suspected, but Caldon and Ignjatovic recently established ([pdf][1]) a formal superexponential lower bound for $f$, at least on an infinite set of formulas.  Their result is phrased for a different infinitary system, $I\Sigma^0_1$, that lies between PRA and $\text{WKL}_0$. $I\Sigma^0_1$ is a fragment of Peano arithmetic, unlike $\text{WKL}_0$; its main difference from PRA is that $I\Sigma^0_1$ allows direct universal quantification over the set of natural numbers during the proof, while PRA does not. 


  [1]: http://www.cse.unsw.edu.au/~ignjat/inst.pdf