Thanks first to Andrej for drawing attention to
my paper on the IVT,
and indeed for his contributions to the work itself.
This paper is the introduction to Abstract Stone Duality
(my theory of computable general topology) for the general mathematician,
but Sections 1 and 2 discuss the IVT in traditional language first.
The following are hints at the ideas that you will find there and
at the end of Section 14.

I think it's worth starting with a warning about the computable
situation in ${\bf R}^2$, where it is customary to talk about fixed
points instead of zeroes.

Gunter Baigger
described
a computable endofunction of the square.
The classical Brouwer thereom says that it has a fixed point,
but *no such fixed point can be defined by a program*.
This is in contrast to the classical response to the constructive
IVT, that either there is a computable zero, or the function
hovers at zero over an interval.
(I have not yet managed to incorporate Baigger's counterexample
into my thinking.)

Returning to ${\bf R}^1$, we have a lamentable failure of classical
and contructive mathematicians to engage in a meaningful debate.
The former claim that the result in full generality is "obvious",
and argue by
quoting random fragments of what their opponents have said in
order to make them look stupid.
On the other hand, to say that
"constructively, the intermediate value theorem fails"
by showing that it implies excluded middle
is equally *un*constructive.

Even amongst mainstream mathematicians several arguments are conflated,
so I would like to sort them out on the basis of
*the generality of the functions* to which they apply.

On the cone hand we have the classical IVT, and the approximate
construtive one that Neel mentions. These apply to *any*
continuous function with $f(0) < 0 < f(1)$.

There are several other results that impose other pre-conditions:

the exact constructive IVT, for non-hovering functions,
described by Reid;

using **Newton's algorithm**,
for continuously differentiable functions
such that $f(x)$ and $f'(x)$ are never simultaneously zero; and

the **Brouwer degree**,
with an analogous condition in higher dimensions.

These conditions are all weaker forms of saying that the function is
an **open map**.

Any continuous function $f:X\to Y$ between compact Hausdorff spaces
is **proper**: the inverse image $Z=f^{-1}(0)\subset X$
of $0\in Y$ is compact (albeit possibly empty).

If $f:X\to Y$ is also an open map then $Z$ is **overt** too.
I'll come back to that word in a moment.

When $f$ is an open map between compact Hausdorff spaces and $Z$
is nonempty, there is a compact subspace $K\subset X$ and an open
one $V\subset Y$ with $0\in V$ and $V\subset f(K)$.

So for real manifolds we might think of $K$ is a (filled-in) **ball**
and $f(K)\setminus V$ as the *non-zero* values that $f$
takes on the **enclosing sphere**.

Could I have forgotten that the original question was about
**computability**?

No, that's exactly what I'm getting at.

In ${\bf R}^1$ an enclosing sphere is a **straddling interval**,
$[d,u]$ such that $f(d) < 0 < f(u)$ or $f(d) > 0 > f(u)$.

The interval-halving (or, I suspect, any computational) algorithm
generates a convergent sequence of straddling intervals.

More abstractly, write $\lozenge U$ if the open subset $U$ contains
a straddling interval.
The interval-halving algorithm (known historically as the
**Bolzano--Weierstrass theorem** or
**lion hunting**)
depends exactly on the property that $\lozenge$ takes unions to
disjunctions, and in particular
$$ \lozenge(U\cup V) \Longrightarrow \lozenge U \lor \lozenge V. $$
(Compare this with the Brouwer degree, which takes disjoint unions
to sums of integers.)

I claim, therefore, that the formulation of the constructive IVT
should be the identification of suitable conditions (more than
continuity but less than openness) on $f$ in order to prove the
above property of $\lozenge$.

Alternatively, instead of restricting the function $f$,
we could restrict the open subsets $U$ and $V$.
This is what the argument at the end of
Section 14
of my paper does.
This gives a factorisation $f=g\cdot p$ of *any* continuous
function $f:{\bf R}\to{\bf R}$ into a proper surjection $p$
with compact connected fibres and a non-hovering map $g$.

To a classical mathematician, $p$ is *obviously* surjective
in the pointwise sense, whereas this is precisely the situation
that a constructivist finds unacceptable.
Meanwhile, they agree on finding zeroes of $g$.

In fact, this process finds **interval-valued zeroes** of
any continuous function that takes opposite signs, which was
the common sense answer to the question in the first place.

The operator $\lozenge$ defines an **overt subspace**,
but I'll leave you to read the paper to find out what that means.

computablefunction f maps the computable reals in the interval [x1, x2] to computable reals, with f(x1)=y1 and f(x2)=y2, then for anycomputablenumber yc between y1 and y2, there is somecomputablenumber xc between x1 and x2 such that the function at f(xc)=yc." (Continuity is defined the same for the computable reals as for the reals, in case that's the difficulty.) – Jason Orendorff Dec 15 '09 at 17:45