CRII: SHF: Codata: A Logical Fusion of Object-Oriented and Functional Programming

CRII：SHF：Codata：面向对象和函数式编程的逻辑融合

• 批准号: 2245516
• 负责人: Paul Downen
• 金额: $ 17.47万
• 依托单位: University of Massachusetts Lowell
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-06-01 至 2025-05-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2245516&HistoricalAwards=false
• 关键词: CRII; SHF; Codata; Logical; Fusion

The programming language used by software engineers can seriously impact how easy it is to express ideas in complex systems. Programmers need positive expressiveness to describe the good things a program should do, as well as negative expressiveness to prevent the bad things a program should never do. Both angles of expressiveness are involved when programmers must satisfy several competing requirements, from low-level needs of managing efficient use of resources to high-level needs of ensuring critical safety and security guarantees. Currently, there are two popular methods for organizing programs to meet these goals --- the object-oriented and functional paradigms --- that use different techniques with their own strengths and weaknesses. Unfortunately, the vast majority of programming languages are stuck within just one of the two paradigms, making it difficult for programmers to harness simultaneously the expressive benefits of both. The novelties of this project are (i) to use new connections between computer programming and the mathematical foundations of logic for the purpose of designing practical, multi-paradigm programming languages, (ii) to develop user-friendly idioms for programmers to utilize the new features from formal logic, and (iii) to apply this logical core as a bridge between high-level and low-level concerns of programs. In contrast to other multi-paradigm languages --- that are typically designed within one paradigm and later bolt on some features of the other --- this project aims to put both paradigms on equal and fair footing by beginning with a logical core where both naturally arise. The project's impacts are (i) to implement a single programming language with a unified design that applies state-of-the-art theoretical research to derive expressive features from both the object-oriented and functional paradigms, and (ii) to develop new techniques suitable for extending existing, popular, programming languages with their missing features.The language developed by this project is based on an understanding of duality that highlights the opposing forces in all computation: inputs versus outputs, call versus response, concrete structures versus abstract patterns. This understanding is based on timeless ideas from a classical logic known as the "sequent calculus," using the Curry-Howard correspondence as a mechanism to transfer ideas from logic to computer science. In this sense, the novel programming ideas implemented here were already discovered, tested, and hardened independently in proof theory, and this project gives them a fresh perspective. The logical foundation of this project is closer to a low-level machine --- making it easier to talk about performance --- while also giving increased expressive power for programming --- via novel organizations of information and control flow, and advanced tools for understanding behavior. Thus, the project aims to strike a balance between the conflicting goals of flexibility --- a hallmark of scripting languages which let programmers modify the fundamentals of the language themselves --- and predictability --- a necessary resource for compiling efficient and well-behaved programs. Special attention will be given to address ubiquitous programming challenges including modularity of compositional components, communication of complex messages between independent entities, and regulating the state of resources limited by time or space. As a side benefit, this methodology may open up a path toward merging the object-oriented paradigm with the proofs-as-programs approach to formally verifying properties of complex software systems and mathematical theorems.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

软件工程师使用的编程语言会严重影响在复杂系统中表达想法的难易程度。程序员需要积极的表达来描述程序应该做的好事，也需要消极的表达来防止程序不应该做的坏事。 当程序员必须满足多个相互竞争的需求时，从管理资源有效使用的低级需求到确保关键安全和安保保证的高级需求，这两个表达角度都涉及到。 目前，有两种流行的方法来组织程序来实现这些目标——面向对象和函数范式——它们使用不同的技术，各有优缺点。 不幸的是，绝大多数编程语言都停留在这两种范式中的一种，这使得程序员很难同时利用这两种范式的表达优势。 该项目的新颖之处在于（i）利用计算机编程和逻辑数学基础之间的新联系来设计实用的多范式编程语言，（ii）开发用户友好的习惯用法，以便程序员利用新的​​语言形式逻辑的特征，以及（iii）应用这个逻辑核心作为程序的高层和低层关注点之间的桥梁。 与其他多范式语言（通常是在一种范式中设计，然后附加另一种范式的某些功能）相比，该项目旨在通过从逻辑核心开始，将两种范式置于平等和公平的基础上。自然产生。 该项目的影响是（i）实现具有统一设计的单一编程语言，该语言应用最先进的理论研究，从面向对象和函数范式中得出表达特征，以及（ii）开发新技术适合扩展现有的、流行的编程语言及其缺失的功能。该项目开发的语言基于对二元性的理解，强调了所有计算中的对立力量：输入与输出、调用与响应、具体结构与抽象模式。 这种理解基于被称为“序列微积分”的经典逻辑的永恒思想，使用柯里-霍华德对应关系作为将思想从逻辑转移到计算机科学的机制。 从这个意义上说，这里实现的新颖的编程思想已经在证明理论中被独立发现、测试和强化，这个项目给了他们一个全新的视角。 该项目的逻辑基础更接近于低级机器——使得谈论性能变得更容易——同时还通过新颖的信息和控制流组织以及先进的工具增强了编程的表达能力用于理解行为。 因此，该项目旨在在灵活性和可预测性这两个相互冲突的目标之间取得平衡——灵活性是脚本语言的标志，它允许程序员修改语言本身的基础知识——可预测性是高效和良好编译的必要资源。表现良好的程序。 将特别关注解决普遍存在的编程挑战，包括组合组件的模块化、独立实体之间复杂消息的通信以及调节受时间或空间限制的资源状态。 作为一个附带好处，这种方法可能开辟一条将面向对象范式与证明程序方法相结合的道路，以正式验证复杂软件系统和数学定理的属性。该奖项反映了 NSF 的法定使命，并被认为是值得的通过使用基金会的智力优势和更广泛的影响审查标准进行评估来获得支持。