Thanks first to Andrej for drawing attention to
<a href="http://PaulTaylor.EU/ASD/lamcra">my paper on the IVT</a>,
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
<a href="https://scholar.google.co.uk/scholar?q=Baigger+fixpunktsatzes">
described</a>
a computable endofunction of the square.
The classical Brouwer theorem says that it has a fixed point,
but <i>no such fixed point can be defined by a program</i>.
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 constructive mathematicians to engage in a meaningful debate.
The former claim that the result in full generality is "obvious",
and argue by
<a href="https://cs.nyu.edu/pipermail/fom/2009-May/013768.html">
quoting random fragments of what their opponents have said in 
order to make them look stupid</a>.
On the other hand, to say that 
"constructively, the intermediate value theorem fails"
by showing that it implies excluded middle
is equally <i>un</i>constructive.

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

On the cone hand we have the classical IVT, and the approximate
constructive one that Neel mentions.  These apply to <i>any</i>
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 <b>Newton's algorithm</b>,
   for continuously differentiable functions
   such that $f(x)$ and $f'(x)$ are never simultaneously zero; and

 - the <b>Brouwer degree</b>,
   with an analogous condition in higher dimensions.

These conditions are all weaker forms of saying that the function is
an <b>open map</b>.

Any continuous function $f:X\to Y$ between compact Hausdorff spaces
is <b>proper</b>: 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 <b>overt</b> 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) <b>ball</b>
and $f(K)\setminus V$ as the <i>non-zero</i> values that $f$
takes on the <b>enclosing sphere</b>.

Could I have forgotten that the original question was about
<b>computability</b>?

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

In ${\bf R}^1$ an enclosing sphere is a <b>straddling interval</b>,
$[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
<b>Bolzano--Weierstrass theorem</b> or
<a href="http://users.ox.ac.uk/~invar/lions.html"><b>lion hunting</b></a>)
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
<a href="http://www.paultaylor.eu/ASD/lamcra/asdivt">Section 14</a>
of my paper does.
This gives a factorisation $f=g\cdot p$ of <i>any</i> 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 <i>obviously</i> 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 <b>interval-valued zeroes</b> 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 <b>overt subspace</b>,
but I'll leave you to read the paper to find out what that means.