As target language for the compilation, a suitable machine language is selected. Our starting point is the instruction set. More abstract levels of machine language might be investigated to ease theoretical considerations. But the target language of the compiler will be the machine language of an existing processor in order to be able to execute generated code on real hardware. The semantics for the machine language will be formalised in an appropriate style to make correctness proofs for compiler specifications feasible. An important aspect in the design of the semantics will be the formalisation of time at the hardware level.