Dear toposophers, With constructivity of real arithmetic back on the front burner for the moment, let P be the ring of bounded power series a0 + a1.x + a2.x^2 + ... with integer coefficients a_i, where the bound is, for each such series, an integer c such that |a_i| < c (3/2)^i / i^(3/2). Let 1-2x generate the ideal I of P. Then the quotient ring P/I turns out to be the field of reals [AMM 105(1998), p.769]. This is more constructive than it might appear, being just an obscure (or clear depending on your upbringing) way of representing reals in a redundant binary notation. The ring P permits fast arithmetic essentially by deferring carries. Carries are "propagated" when needed by quotienting by I, which works by collapsing every formal power series to one all of whose coefficients other than a0 are either 0 or 1 and which has infinitely many 0s (equivalently, no infinite run of 1's). In this view of things, a real is understoood as an integer (a0) plus a binary fraction in [0,1) (the rest of some "binary" formal power series, meaning one with a_i = 0 or 1 for i > 0 and infinitely many 0s). A general formal power series without this restriction to 0 and 1 then constitutes a redundant representation of a real, which can be made irredundant when needed (e.g. when comparing with <) by quotienting by I. An intuitively clear but less constructive view is to evaluate each series at x = 1/2, the root of 1-2x, noting that any series bounded as above converges absolutely there. Series identified by I are those that evaluate to the same real at x = 1/2. What is nonconstructive about this is that direct evaluation of an infinite series at a point requires infinite time, no matter how large and parallel the infinite circuit computing it may be. In contrast, P and P/I are more constructive in the following sense. Addition and subtraction in P require circuit depth O(1) using an infinite circuit whose gates perform integer addition and subtraction (just do it coordinatewise). Reduction mod I takes longer, but there is a variant of the above in which it is fast enough. Instead of the field R we settle for just the group R, and instead of |a_i| < c (3/2)^i / i^(3/2) we settle for simply |a_i| < c. In this case any given series can be reduced (same generator 1-2x) to the above normal form in circuit depth log_2(c) (nice exercise), a finite quantity despite the series itself being of infinite length and fluctuating arbitrarily within ±c. Multiplication is problematic for two reasons. First it obliges the weaker bound, complicating reduction. Secondly it is a convolution, complicating arithmetic even when carry propagation is deferred. I don't see obvious solutions to either of these problems. On the other hand I have no a priori reason to suppose that these circuit-theoretic complications of passing from R as a group to R as a ring or field would be reflected in suitably constructive topos-theoretic developments of these notions. Vaughan Pratt