In the literature on constructive and linear logic it is the other way around, although $\to$ doesn't strictly belong to either group because it isn't monotone. Troelstra's Contructivism in Mathematics defines the almost negative formulas of Heyting arithmetic as formulas that have no $\vee$ and limited use of $\exists$.
In linear logic the terminology made Wikipedia (http://en.wikipedia.org/wiki/Linear_logic). The standard translation of intuitionist logic into linear logic confirm that $\bot$,$\vee$ and $\exists$ are positive.
The terminology may be linked to the school of Logical Positivism in philosophy, because examples prove positive formulas and refute negative formulas.
Linear logic started with Girard's observation that intuitionistic implication is the composition of two substructural connectives in the following way.
$$A\to B\iff !A\multimap B$$
Here $!$ is a connective that allows weakening and contraction, while linear implication $\multimap$ requires that every antecedent is used exactly once in the derivation of the consequent.
The category-theoretic explanation of the polarities in linear logic is that positive connectives are left adjoints and negative connectives are right adjoints between certain categories of formulas and proofs. This works well in linear logic because conjunction $\land$ splits up into two connectives. The negative $\&$ is the Cartesian product--i.e. the right adjoint of the diagonal--while the positive $\otimes$ is the tensor product--i.e. $-\otimes A$ is right adjoint to $A\multimap-$ for each formula $A$. The $!$ connective makes up for the difference: $$!(A\& B)\iff !A\otimes !B$$
