This talk is a report about a joint project of the universities at Karlsruhe, Kiel and Ulm on how to get correct compilers for realistic programming languages. Arguing about compiler correctness must start from a compiling specification describing the correspondence of source and target language in formal terms. We have chosen to use abstract state machines (ASMs) to formalize this correspondence. This allows us to stay with traditional compiler architectures for subdividing the compiler task. A main achievement is the use of program checking for replacing large parts of compiler verification by the much simpler task of verifying program checkers. This project will hopefully produce a verified compiler from most of Sather-K, the Karlsruhe version of Sather, into machine-code of DEC-Alpha processors within the foreseeable future.