I can't comment about the programming language aspect, but here is the logical aspect. A sequent is an expression of the form
$$ A_1,\ldots,A_n \vdash B_1,\ldots,B_m $$
whose meaning is "if $A_1,\ldots,A_n$ hold then one of $B_1,\ldots,B_m$ holds", that is
$$ (A_1 \land \cdots \land A_n) \to (B_1 \lor \cdots \lor B_m). $$
Sequent calculus is nice since its laws enjoy a certain symmetry between the two sides that reflects the de Morgan symmetry between AND and OR.
Weakening is the law that states that you can a formula to either side of a sequent. That is, if a sequent $\Gamma \vdash \Delta$ is true (where $\Gamma,\Delta$ are sequences of propositions), then for every formula $X$, both sequents $\Gamma,X \vdash \Delta$ and $\Gamma \vdash \Delta,X$ also hold.
Contraction states that if a formula appears twice one of the sides, then an equivalent sequent is obtained by removing the duplicate. That is, if $\Gamma,X,X \vdash \Delta$ then also $\Gamma,X \vdash \Delta$, and similarly for duplicates on the other side.
One more structural rule, permutation, allows us to reorder formulas: if $\Gamma,X,Y,\Delta \vdash E$ then also $\Gamma,Y,X,\Delta \vdash E$, and the same for the other side.