If the contrapositive of a statement can be proven directly, can that statement itself necessarily be proven directly? So to be more formal: Given statements $A$ and $B$ such that a direct proof exists for $\neg B \implies \neg A$, is there necessarily a direct proof for $A \implies B$. By "direct proof," I mean a proof that does not ever assume $\neg B$.
Thanks in advance for any answers!
 A: You say "I mean a proof that doesn't use contradiction, nor the contrapositive." So does that mean modus tollens is allowed in a direct proof? And conditional proof? And the double negation rules? 
If so we can argue

$$\neg B \to \neg A\\
\quad | \quad \ \ \ A\\
\quad | \quad \neg\neg A\\
\quad | \quad \neg\neg B\\
\quad | \quad \ \ \ B\\
A \to B$$

And so we can convert a direct proof of the first into a direct proof of the second ....
If you think that's a cheat, you are going to have to say a LOT more about what you mean by a "direct proof".
A: If you're talking about intuitionism, then the answer is no.
First, see that the other way works fine: $(a\implies b)\vdash (\neg b\implies \neg a)$:
Premise: $a\implies b$.
Assume $\neg b$.
Assume $a$.
By modus ponens and the premise, $b$.
Since $\neg b$, this is a contradiction.
Thus $\neg a$.
By implication, $\neg b \implies \neg a$. QED.
Now see what goes wrong the other way:
Premise: $\neg b \implies \neg a$.
Assume $a$.
Trying the same thing as before, assume $\neg b$.
Following the same reasoning, we get to … $a\implies \neg\neg b$, which isn't intuitionistically the same.
In fact, we can go further:
Accept the principle that $\neg b \implies \neg a\vdash a\implies b$.
Take my word for it that $\neg (a\lor \neg a)\implies \bot \implies \neg \top$ holds intuitionistically, where $\top$ is, say, $\neg(a\land \neg a)$.
Then applying the "risky" contraposition principle, $\top \implies a \lor \neg a$, so by modus ponens, $a\lor \neg a$.
That is, from the "reverse" contraposition principle, we derive excluded middle.
A: If [($\lnot$A$\rightarrow$$\lnot$B)$\rightarrow$(B$\rightarrow$A)] comes as either an axiom or a theorem of your system, then if you have a proof of (¬B$\rightarrow$¬A), you can write a direct proof of (B$\rightarrow$A) by using the rule of detachment.
A: Here is the question:

So to be more formal: Given statements A and B such that a direct proof exists for ¬B⟹¬A, is there necessarily a direct proof for A⟹B. By "direct proof," I mean a proof that does not ever assume ¬B.

We are given the following premises: $A$, $B$ and $\neg B \to \neg A$. The goal is to prove $A \to B$.  Here would be a proof using a Fitch-style proof checker:

The three premises are listed on on the first three lines. On line 4 I assume $A$. On line 5, I use reiteration to derive (reiterate) the second premise. On line 6 I use conditional introduction to derive the goal.
All one needs is the truth of $B$.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
