Moebius: Logical Principles for Type-Safe Meta-Programming

点击翻译按钮获取中文摘要

Software is everywhere around us and our society increasingly depends on its well-functioning. However, building safe and efficient software often must balance very different competing demands. Good software design practices call for abstractions that separate programs into modular components that can be exchanged, reused, and verified independently from each other. To achieve the desired performance, however, it is critical to customize the code depending on the application domain. These two goals seem at odds. One approach to achieve both is meta-programming -- the art of writing programs that generate and manipulate other programs. This opens the possibility to exploit domain-specific knowledge to build high-performance programs and complements general program optimizations a compiler would employ. Unfortunately, writing safe meta-programs remains very challenging and frustrating, as traditional testing techniques can only be used when eventually running the generated code, but not at the time when the code is generated. To make it easier to write meta-programs, tools that allow us to detect errors during code generation -- instead of when running the generated code -- are essential. Our long-term vision is to introduce a new programming paradigm for safe meta-programming where we statically verify safety guarantees about the code generation and the code itself. Here, almost all debugging is done during code generation instead of when executing and testing the generated code at a later stage. In the long-term, this will make writing and maintaining meta-programs substantially easier. It will allow us to exploit the full potential of meta-programming without sacrificing reliability of and trust in the software we are producing and running. Our long-term goals are: 1) to ensure that we can correctly compose generated code with other programs; 2) to provide programmers with appropriate abstractions that allow them to generate and to smoothly analyze generated code fragments subsequently by pattern matching on code; 3) to make it routine work for programmers to certify functional correctness of generated code. To achieve these goals, we pursue the following short-term objectives: to develop a syntactic and semantic foundation for type-safe meta-programming based on modal logic and to implement and evaluate a proof-of-concept prototype using realistic applications. This research program has the potential to impact a wide range of technologies: from generating optimized code for matrix computations in machine learning to cryptographic message authentication in secure network protocols, which sit at the heart of Google Chrome. These examples illustrate the critical role meta-programming currently plays in research and industrial applications. Our research hence ensures the continued growth of a safe and competitive IT infrastructure and strengthens Canada's leadership in the technology sector.