After 40 years of practice and theory in compiler construction and 30 years of experience and teaching in software engineering we still observe that safetycritical high-level language programs are certified only together with the corresponding machine code. The reason is that certification institutions do not trust any compiler. And they are quite right: whereas errors detected in processor hardware are generally perceived as sensations, errors in software, even in system software, are commonplace.
It is high time to reverse this trend. Computer scientists should concentrate their abilities, experiences, and insights on the safe mastery of realistic system software. This particularly concerns realistic compilers for realistic programming languages running on hardware processors, as correct compilers play a central role in the construction of trustworthy application and system programs. Both application programmers and system software engineers need trusted development environments that permit them to concentrate on software specification and high-level implementation instead of wasting their time again and again with compilation problems and machine code inspection.
This book presents the verified design of a code generator translating a prototypic real-time programming language to an actual microprocessor, the Inmos Transputer. Unlike most other work on compiler verification, and with particular emphasis on modularity, it systematically covers correctness of translation down to actual machine code, a necessity in the area of safety-critical systems. The formal framework provided as well as the novel proof-engineering ideas incorporated in the verified code generator are also of relevance for software design in general.