As long as \epsilon != 0 one can make rational_of(\Pi, \epsilon) an arbitrarily close approximation of \Pi, without the need for infinity. In fact that is precisely what we use in practice, by that I mean computation.
Ultimately it comes down to a trade off. Which axiomatic system does one to work in ? Introducing infinity does have its fair share of warts (by warts I mean consequences that flies in the face of intuition).
How do you approximate pi in this way without making use of an infinite series? Or are you saying that an approximation that doesn't use an infinity is fine even if an infinity was used to arrive at it?
You can truncate the series at an appropriate place of your choosing. But yes, \Pi as a number does not even exist unless you add the Reals, so that would need infinity. What I am saying is, one can work with the Rationals.
Ultimately it comes down to a trade off. Which axiomatic system does one to work in ? Introducing infinity does have its fair share of warts (by warts I mean consequences that flies in the face of intuition).