Lambda calculus is an abstraction of computation - but it needs to be defined, somehow, and you can use prose ("a term is a character representing a parameter or value, an application of a term to another term is expressed by writing the two terms with a space between them") or rules ("term := x | y | z ; app := x x") where the rules are an abstraction of the ideas in the prose.
Similarly you can describe substitution with words or a formal syntax. The latter is usually more concise and less ambiguous.
Lambda calculus is arguably far more abstract because often type theories imply a lot of implrmentation constraints, which makes sense since that's kind of the piount.
Similarly you can describe substitution with words or a formal syntax. The latter is usually more concise and less ambiguous.