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

点击翻译按钮获取中文摘要

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.