An automatically generated and provably correct compiler for a subset of Ada

We describe the automatic generation of a provably correct com-piler for a non-trivial subset of Ada. The compiler is generated from RISC machine language that currently is assembled into code for the SPARC and the HP Precision Architecture. The generated code is an order of magnitude better than what is produced by compilers gener-ated by the classical systems of Mosses, Paulson, and Wand. The use of action semantics makes the processable language specification easy to read and pleasant to work with