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基础设施的持续增长，并加强了加拿大在技术领域的领导地位。