Immutable (or "pure") and functional are two very different things. State-machine-based programming languages -- usually called synchronous languages (note that TLA+ is not a programming language) -- may be pure, but are not functional. Functional means that you model a computation as a function. In synchronous language and in TLA, a computation is not a function but a behavior -- a sequence of states. You can say things like "no matter what happens, the value of x is always greater than 0", or "if y is ever negative, then z must later become negative, too". In addition, in TLA the next state is not a function of the current state; (state, nextstate) is a relation, so a state can have multiple possible next state, chosen nondeterministically. This is essential when modeling nondeterministic programs (like those involving concurrency or distribution), or even when modeling deterministic program at a high level of abstraction where you don't care about the details ("the algorithm will do either A or B for some reason I don't care about").