Moebius: Logical Principles for Type-Safe Meta-Programming

软件无处不在，我们的社会越来越依赖于它的良好运作。然而，构建安全和高效的软件往往必须平衡非常不同的竞争需求。好的软件设计实践需要将程序分离成模块化组件的抽象，这些组件可以相互独立地交换、重用和验证。但是，要实现所需的性能，根据应用程序域自定义代码至关重要。这两个目标似乎是不一致的。实现这两个目标的一种方法是元编程--编写生成和操作其他程序的程序的艺术。这为利用特定领域的知识来构建高性能程序提供了可能性，并补充了编译器将采用的一般程序优化。不幸的是，编写安全的元程序仍然非常具有挑战性和令人沮丧，因为传统的测试技术只能在最终运行生成的代码时使用，而不能在代码生成时使用。为了使编写元程序更容易，允许我们在代码生成过程中检测错误的工具-而不是在运行生成的代码时-是必不可少的。我们的长期愿景是为安全元编程引入一种新的编程范式，在这种范式中，我们静态地验证代码生成和代码本身的安全保证。在这里，几乎所有的调试都是在代码生成期间完成的，而不是在稍后阶段执行和测试生成的代码时完成的。从长远来看，这将使编写和维护元程序变得更加容易。它将使我们能够充分利用元编程的潜力，而不会牺牲我们正在生产和运行的软件的可靠性和信任。我们的长期目标是：1）确保我们可以正确地将生成的代码与其他程序组合; 2）为程序员提供适当的抽象，允许他们随后通过对代码的模式匹配来生成并平滑地分析生成的代码片段; 3）使程序员验证生成的代码的功能正确性成为日常工作。为了实现这些目标，我们追求以下短期目标：开发基于模态逻辑的类型安全元编程的语法和语义基础，并使用实际应用程序实现和评估概念验证原型。这项研究计划有可能影响广泛的技术：从机器学习中的矩阵计算生成优化代码到安全网络协议中的加密消息身份验证，这些都是Google Chrome的核心。这些例子说明了元编程目前在研究和工业应用中的关键作用。因此，我们的研究确保了安全和有竞争力的IT基础设施的持续增长，并加强了加拿大在技术领域的领导地位。

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.