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.