What are the 2 definitions of substitution used in TAPL? for what purposes?

$[x\to s]t$ -> Useful for mathematical reasoning, proofs.

De Bruijn's notation -> Notationally heavier, but useful for compiler's implementation.