What is a "contradiction" in constructive logic?
It is immaterial whether we speak about constructive or classical logic in this situation. If you read your questions again, you will see that they apply to boths kinds. The only difference that we need to take notice of is the presentation of negation $\lnot A$. It can be presented in several ways classically, but intuitionistically it is best to use it as an abbreviation for $A \Rightarrow \bot$ (which is precisely what Bob Harper is hinting at in the quoted paragraph). But let us not confuse negations and contradictions.

In both cases, a contradiction is a situation in which we have managed to prove falsity $\bot$. How could we derive $\bot$ in a sensible way? Well, from an inconsistent set of hypotheses, that wold be a sensible way to do it.

You have no discretion to "declare" a contradiction. You must prove that a given set of hypotheses is contradictory by deriving $\bot$. For instance, if $a = b$ and $\lnot (a = b)$ then we may use the fact that $\lnot (a = b)$ is an abbreviation for $(a = b) \Rightarrow \bot$ and conclude $\bot$ by modus ponens.