] specifies that in expr occurrences of the symbols x, y, ... should be replaced by , , ... .
With allows you to define local constants.
With replaces symbols in expr only when they do not occur as local variables inside scoping constructs.
You can use With[
] as the right-hand side of a transformation rule with a condition attached.
With has attribute HoldAll.
With is a scoping construct (see Section A.3.8).
With constructs can be nested in any way.
With implements read-only lexical variables.
See the Mathematica book: Section 2.6.2.
See also: Module, Block, ReplaceAll.
Even though t is set inside With, it keeps its global value.