That's not saying that the Word is a function in the programming sense. It's saying that, if you're doing static analysis of a program, there is a mathematical

That's not saying that the Word is a function in the programming sense. It's saying that, if you're doing static analysis of a program, there is a mathematical function that models the Word's behavior. In particular, it's doing the 'standard' trick where any computer program can be modeled as a function whose input is the entire computer (and possibly outside resources like the network), and whose output is that computer updated with any state changes that might have occurred. But that function that describes the word's behavior on the computer isn't the same as the word itself. The word's input is the few words under it on the stack, and its input is something that goes on the stack. The function's input is the entire stack, and its input gets fed into the next function. You're correct that you could right an implementation that reifies this concept, if you're so inclined. But that's still not the same thing. The 'function' is still on the meta-language level, not the language level where the word is.