Moebius: Logical Principles for Type-Safe Meta-Programming

Moebius：类型安全元编程的逻辑原理

• 批准号: RGPIN-2022-03224
• 负责人: Pientka, Brigitte
• 金额: $ 4.66万
• 依托单位: McGill University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2022
• 资助国家: 加拿大
• 起止时间: 2022-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=750376
• 关键词: Moebius; Logical; Principles; Type; Safe

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.

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