Can the principle of explosion be removed from constructive logic?

Classical logic has the theorem ($p\wedge\lnot p)\rightarrow q$, which I will call EFQ ("ex falso quodlibet"). Constructive logic often has the principle built in, in the form of an axiom $\bot\rightarrow q$ which one can use to prove EFQ via $(p\wedge\lnot p)\rightarrow \bot$.

Suppose one takes some usual system of constructive logic and deletes $\bot\rightarrow q$. Then although $(p\wedge\lnot p)\rightarrow \bot$ is still provable, there is no longer any way to eliminate $\bot$, so one can't get anything further from a contradiction. Or so I believe; did I miss anything? Can one still deduce EFQ? If one deletes the $\bot$-elimination rule as I suggested, does the resulting logic depend on which equivalent formalization one starts with?

This system is no longer complete with respect to the usual model (subsets of $\Bbb R$), but perhaps one can adjust the model a little bit and get a slightly different model with respect to which this logic is complete and consistent.

Is there anything obviously wrong with this logic that I've overlooked? Is it discussed anywhere? (I don't remember reading about it in Priest's book In Contradiction, but I read it some years ago and may have forgotten.)

It is called ex falso axiom.

The logic obtained from removing it is called minimal logic and is well studied. In this logic, $\bot$ act just like another atomic formula with no particular property.

In real theories we can often replace $\bot$ with an explicit formula that would play its role, e.g. in Heyting arithmetic, we can derive arbitrary formulas from $0=1$ without any need for $\bot$ or the ex falso axiom.

Troelstra and van Dalen's "Constructivism in Mathematics" has a through discussion of the logic (IIRC).

This is studied under the name "Paraconsistent logic": https://en.wikipedia.org/wiki/Paraconsistent_logic

As the article describes, you also need to eliminate at least one other rule as well, in order to get anything worthwhile. Otherwise, as in student's answer, you can still effectively prove nearly anything from false.

We still have $\lnot$ introduction: under assumption $p$, a derivation of $\bot$ gives us $\lnot p$. So in constructive/ intuitionistic logic, if we have a proof of $\bot$ we can derive $\lnot p$ for any $p$ whatsoever. Such a logic can derive "almost" anything, and in particular, for any $p$ it proves, it will also prove $\lnot p$. And in classical logic, since we have double negation elimination, we have full EFQ: derive first $\lnot p$, then $\lnot \lnot p$, then apply DNE to get $p$. So one still gets a lot from $\bot$ without further restrictions on the proof system. As you might know from reading Priest, efforts have been made towards this, for instance $p \rightarrow q$ only when there is some relation between $p$ and $q$.

Robin Houston points out that if we can deduce $q$ from $p\vee q$ and $\lnot p$, then we can deduce $q$ from $p\wedge \lnot p$.