Strength of Bishop style constructive mathematics vs $\mathsf{RCA}_0$ This question came out of this other MO question of mine.  My question is

Is there a formal comparison between $\mathsf{RCA}_0$ and $\mathsf{BISH}$ (Bishop style constructive mathematics as used in constructive reverse mathematics)?

More specifically,

Is $\mathsf{BISH}$ strictly weaker than $\mathsf{RCA}_0$ (or $\mathsf{RCA_0}$ plus full induction) when formalized and restricted to second order sentences of arithmetic?
(Update: I wasn't entirely clear, I meant to ask if everything provable in $\mathsf{BISH}$ is provable in $\mathsf{RCA_0}$ plus full induction.  Obviously, nonconstuctive principles like LEM are provable in $\mathsf{RCA_0}$ but not in $\mathsf{BISH}$.)

I am sure people have thought of this, but I couldn't find a resource.
Also, I imagine there could be a lot of caveats.  I don't know much about Bishop-style constuctivism, but I gather the community doesn't like formal theories or models, which are generally needed for such comparisons.  However, I know others are interested in such things, and I believe there are formalizations of $\mathsf{BISH}$ that at least get close to the intuitive idea.
Also, this question can be answered without formal theories:

Is there a theorem known to be constructively provable (in the informal style of Bishop), that is not provable in $\mathsf{RCA}_0$ (or $\mathsf{RCA}_0$ plus full induction)?

 A: Maybe it is interesting that for $CT$ (Church thesis) $BISH+CT$ is consistent, but $RCA_0\vdash \neg CT$. By $CT$ I mean axiom scheme of $CT$ for every formula.
$CT-scheme$: For every first order formula $\psi(x,y)$, $\forall x \exists y \psi(x,y)\rightarrow \exists e\forall x\exists y(\psi(x,y)\land \phi(e,x,y)$ where $\phi(e,x,y)$ is kleene predicate.
Also let $U(e,x,y)$ be a first order formula such get godel number of a formula like $\eta(x,y)$ in $e=\ulcorner \eta(x,y) \urcorner$, gets $x,y$ and simulates $\eta(x,y)$, then $CT$ can be formalized in one axiom like this:
$$CT:=\forall u\exists e(\forall x\exists y U(u,x,y)\rightarrow \forall x\exists y(U(u,x,y)\land \phi(e,x,y)))$$
Define $$h(n)=\left\{\begin{matrix} 1,\exists x\phi(n,n,x)\\  0, \forall x \neg \phi(n,n,x) \end{matrix}\right.$$
This function can represent by formula $H(n,y):=(\exists x\phi(n,n,x)\land y=1)\lor(\forall x\neg\phi(n,n,x)\land y=0)$, trivially $RCA_0\vdash \forall n \exists y H(n,y)$, therefore $RCA_0\vdash \neg CT$, but $BISH+CT\nvdash \bot$, similar arguments work if we take axiom scheme of $CT$ instead of $CT$
A: The intermediate value theorem seems to be provable in $RCA_0$ but is certainly not provable in the usual form in $BISH$. I am relying on Wikipedia.
A: I believe BISH includes the Fan Theorem, which, being the contrapositive of weak König's lemma, is not provable in $RCA_0$.
A: Wikipedia thinks RCA roughly corresponds to BISH.
Joan Moschovakis' slides give a recent overview of formal constructive reverse mathematics.
A: BISH famously includes the full axiom of choice scheme (in the functional language of second-order arithmetic), which is utterly weak in that context but very strong when combined with the law of the excluded middle. This is precisely the context in which Bishop wrote that the axiom of choice follows from "the very meaning of existence". 
Thus there are formulas of second-order arithmetic provable in BISH that are not even provable in $Z_2$, the system of clasical second-order arithmetic with full induction and comprehension.  
A: Here is a reference for "$\operatorname{RCA}_{\hspace{.01 in}0}$ proves the intermediate value theorem".
Let $\; f : \mathbb{R} \to \mathbb{R} \:$ be given by $\;\; f(x) \: = \: (2\hspace{-0.03 in}\cdot\hspace{-0.03 in}x)+|\hspace{.02 in}x\hspace{-0.03 in}-\hspace{-0.04 in}1|-(\hspace{.01 in}|\hspace{.02 in}x\hspace{-0.03 in}-\hspace{-0.04 in}1|+h) \:\:\:$,

for some real number $h$ such that $\; h \approx 0\:\:$.

$\:f(-2) \approx -1 < 0 < 1 \approx f(2) \:$, $\:$ so the intermediate value theorem applies to $\:f$.

If $\: h < 0 \:$ then all roots $z$ of $\:f$ are such that $\; z < -1\:\:$.

If $\: 0 < h \:$ then all roots $z$ of $\:f$ are such that $\; 1 < z\:\:$.

Intuitively, it follows from that one cannot prove 'constructively' that $\:f$ has a root.

However, since I know very little about $\operatorname{BISH}$, I don't know how to

convert that to "$\operatorname{BISH}$ doesn't prove the intermediate value theorem".
A: LPO is certainly not true in $\mathsf{BISH}$, but I believe it can be formalized and proved in $\mathsf{RCA}_0$.
I don't know if there's any agreed upon theory for formalizing $\mathsf{BISH}$ but there are formal theories used for constructive mathematics that have higher consistency strength than $\mathsf{RCA}_0$. For instance, $\mathsf{CZF}$ has the same consistency strength as $\mathsf{ID}_1$. In particular, it proves that $\mathsf{RCA}_0$ is consistent.
