Admissibility of Harrop's rule, computationally It is obvious that the following formula is not a theorem of
intuitionistic propositional calculus (IPC).
$$
  (\neg A \; \to \; B \vee C) \;\; \to \;\;
  ((\neg A \; \to \; B) \vee (\neg A \; \to \; C))
$$
It can be easily understood by considering Heyting semantics. Indeed,
if you only have a function that maps any proof of $\neg A$ to either a
proof of $B$ or a proof of $C$, you can neither build a function that
maps any proof of $\neg A$ to a proof of $B$ nor a function that maps any
proof of $\neg A$ to a proof of $C$.
The Harrop's rule below is however admissible in IPC.
$$
  \displaystyle
  \frac{
  \neg A \; \to \; B \vee C}{
  (\neg A \; \to \; B) \vee (\neg A \; \to \; C)
}
$$
How can it be understood from a computational (Heyting semantics) point of view?
 A: Suppose $IPC\vdash \neg A \to B\lor C$. Therefore by BHK interpretation there exists a function $f$ that converts a proof of $\neg A$ into pair $\left < a,b\right >$ where $a$ is 0 and $b$ is a proof of $B$ , or $a$  is 1 and $b$ is a proof of $C$. Therefore a proof of $(\neg A \to  B) \vee (\neg A  \to  C)$ is a pair like
$$ \left <a', b' \right >=\begin{cases}\left <0,0 \right >& \forall p\exists u (\vdash_u A \:\land\: \nvdash_{p(u)} \bot) \\ \left <i,\left < C_m \right > \right > & \exists p(\forall u(\vdash_u A \to \: \vdash_{p(u)} \bot)\land f(\left <p \right >)=\left < i, m \right >)\end{cases}$$
Where $\vdash_p \phi$ means $p$ is a proof of $\phi$, $C_m(x)=m$ is a constant function and $\left < p \right >$ is code of function $p$.
Also $\left <a',b' \right >$ is constructively well-defined because weak completeness of $IPC$ with respect to the finite Kripke models can be proved constructively, therefore all we need is checking a finite number of finite Kripke models to find whether $\exists u(\vdash_u \phi)$ or not.
A: The way I understand it is as follows. The most general formula
$
  (\neg A \; \to \; B \vee C) \;\; \to \;\;
  ((\neg A \; \to \; B) \vee (\neg A \; \to \; C))
$
is not derivable in IPC, because it is not an intuitionistic truth, like you said. 
In fact, we can find `almost intuitionistic' Brouwerian counterexamples outside of IPC. For instance if we look at HA + MP and take
$R(n):= 1 \ \mbox{if the first block of 99 consecutive 9's}\\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \mbox{in the decimal expansion of $\pi$ ends at place $n$}$
$R(n):= 0\ \ \mbox{else}$
$A=\forall n [R(n)=0]$ $\ \ \ B= \exists n [R(2n)=1]$
$\ \ \ C= \exists n [R(2n+1)=1]$
Then we see that $\neg A\to B\vee C$ (using MP). But both $(\neg A \; \to \; B)$ and $(\neg A \; \to \; C)$ are elusive. The interesting thing here is, that if HA really proves $\neg A$, then without MP already HA proves `there is $m$ with $R(m)=1$'. This since HA is closed under Markov's Rule, therefore proving $\neg\neg\exists n[P(n)]$ for decidable $P$ in HA allows one to deduce something about the structure of the proof, from which one can find a proof in HA of $\exists n [P(n)]$. This is a proof-theoretical property of the formal system HA.
Similarly, if in IPC we have formulas $A,B,C$ such that IPC proves $(\neg A \; \to \; B \vee C)$, then we know from the proof-theoretical properties of IPC that we can either find a proof in IPC of $(\neg A \; \to \; B)$ or of $(\neg A \; \to \; C)$.
So both computationally and semantically, this Harrop's Rule (also called Independence of Premise Rule, or IPR) being admissible for IPC should be seen as a statement about certain properties of the formal system IPC. 
A nice reference is Rosalie Iemhoff's paper On the rules of intermediate logics.
Addendum: 
It just occurred to me that the question might be asking for an informal semantical/computational explanation why IPC has this property. In that case, consider that in general we cannot extract numerical existence from a negated formula $\neg A$. Therefore, if for a formula $A$ in IPC we deduce that $\neg A$ implies $\exists n\in\{0,1\} [(n=0\to B)\wedge (n=1\to C)]$, then we must have a means to pinpoint this $n$ without having to first prove $\neg A$. And that is precisely Harrop's rule IPR.
This is also why we need Markov's Principle (MP) in the counterexample above: to extract numerical existence from the negated formula $\neg\forall n[R(n)=0]$ which is equivalent to $\neg\neg\exists m [R(m)=1]$
