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

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

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.