A contradiction is usually represented as $A \land \lnot A$. It's typical in intuitionistic logic to define $\lnot A$ as $A \Rightarrow \bot$. It's clear we can derive $\bot$ from $A \land \lnot A$. Ultimately, a contradiction will be a hypothetical derivation of $\bot$ as the very definition of $\lnot$ suggests. It will be hypothetical because otherwise your logic is inconsistent.
The point Harper is making is that to prove something is to have a proof and to refute something is to have a proof that it implies $\bot$. However, you can easily be in the situation that you can (meta-logically) prove that you are unable to provide either a proof or refutation. In such a situation, the proposition is neither constructively true nor false.
A way to understand classical logic and contrast it to the above is the following (essentially Kolmogorov's double negation interpretation): we say a proposition is false if it implies a contradiction, i.e. it implies $\bot$. A proposition is true if we can prove that it can't be contradicted, i.e. we can show assuming it is false leads to a contradiction. In symbols, $A$ is false in this sense if $A \Rightarrow \bot$, as usual. $A$ is true in this sense if $\lnot A \Rightarrow \bot$, i.e. $\lnot \lnot A$ is provable. You can show that the the Law of the Excluded Middle holds constructively if we interpret "true" and "false" in this sense. That is, you can prove that $\lnot \lnot (\lnot \lnot A \lor \lnot A)$ holds constructively. More compactly, you can show $\lnot \lnot \lnot A \Rightarrow \lnot A$. With this notion of "true" and "false", we can say that a proposition is true if we can prove that no refutation exists. By contrast, constructively a proposition can fail to be constructively true even if we can demonstrate within the system that no refutation can exist.