Abstract Machine
An abstract machine is a theoretical model of computation that specifies the operational semantics of a programming language through a set of states and transition rules, without committing to the details of physical hardware. Unlike the Turing machine, which is a model of what can be computed, an abstract machine is a model of how a program executes — an intermediate layer between high-level language semantics and low-level implementation. Examples include the STG machine for Haskell, the Java Virtual Machine for Java, and the LLVM intermediate representation that serves as a compiler backend.
The power of abstract machines lies in their ability to make compiler optimizations and runtime behavior independently analyzable. By fixing a machine model, language designers can prove properties about program execution — correctness of optimizations, safety of garbage collection, bounds on space usage — without reference to the chaotic variety of real processors. The abstract machine is the contract between the language semantics and the implementation; everything above it is mathematics, everything below it is engineering.