Guaranteed optimization for domain-specific programming

Abstract

For software engineering reasons, it is often best to provide domain-specific programming environments in the context of a generalpurpose language. In our view general-purpose languages are not yet general-purpose enough, and progress needs to be made before we can provide domain-specific languages that are both fast and safe. We outline some goals in this regard, and describe a possible implementation technology: guaranteed optimization, a technique for building compilers that provide proven guarantees of what optimizations they perform. Such optimizers can provide capabilities similar to staged languages, and thus provide the relevant performance improvements. They can also function as decision procedures, suggesting an approach of ‘optimizers as theorem provers,' in which optimizing compilers can be used to check domainspecific safety properties and check proofs embedded in programs.