SHF: Medium: Fiat: Correct-by-Construction and Mostly Automated Derivation of Programs with an Interactive Theorem Prover

SHF：Medium：Fiat：使用交互式定理证明器进行构造正确和大部分自动推导程序

• 批准号: 1512611
• 负责人: Adam Chlipala
• 金额: $ 80万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-09-01 至 2020-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1512611&HistoricalAwards=false
• 关键词: SHF; Medium; Fiat; Correct; Construction

Title: SHF: Medium: Fiat: Correct-by-Construction and Mostly Automated Derivation of Programs with an Interactive Theorem ProverTo scale to ambitious software-development tasks, programming languages must provide features for abstraction and modularity. Large advances in programming productivity have often come via new features of that kind. This project investigates new program-structuring ideas based fundamentally on machine-checked mathematical proofs. More specifically, through the design of a prototype system Fiat within the Coq proof assistant, the project studies how to derive efficient programs automatically from logical specifications. Programmers may package new notations and associated styles of automation as libraries, and a single program may mix notations, automatically benefiting from the combination of all of their associated automation for deriving efficient programs. In this way, Fiat makes it possible to split a program into parts for functionality and performance, with strong guarantees that bugs in the performance parts can never violate the requirements in the functionality parts. The intellectual merits are widely applicable new ideas in modular program structuring, with strong formal guarantees of correctness. The project's broader significance and importance are based on the potential to improve programmer productivity dramatically, for software projects in a wide variety of contexts; and the project also studies how the idea of mostly automated refinement from specifications can be integrated into introductory programming and discrete-math classes, to drive home the value of logical notation in programming.The primary case-study domain in the project is practical Internet servers, such as for domain-name lookup or delivery of electronic mail. The goal is to develop Fiat versions of these key services, deriving efficient executable code automatically. Past work on deriving data layers from specifications in the style of SQL is being extended, in addition to exploration of other domains for specification and automated derivation, such as synthesis of parsers from grammars, to use for the protocols that servers speak, the configuration files that they read, etc. Beyond studying how such new libraries may be constructed and composed, the project also investigates how to push the synthesis process to lower abstraction levels than in our prototype implementation, which generates functional programs. The improved Fiat system will derive assembly programs, enabling choice of more effective optimizations thanks to more direct control of machine resources, integrating with the Bedrock Coq library for verified multilanguage programming.

题目：SHF: Medium: Fiat：基于交互式定理的程序构造更正和大部分自动化派生为了扩展到雄心勃勃的软件开发任务，编程语言必须提供抽象和模块化的特性。编程生产力的巨大进步往往来自于这类新特性。本项目主要研究基于机器检验数学证明的新的程序结构思想。更具体地说，通过Coq证明助手中的原型系统Fiat的设计，研究了如何从逻辑规范中自动导出高效的程序。程序员可以将新的符号和相关的自动化风格打包为库，并且单个程序可以混合符号，自动地从所有相关的自动化组合中受益，从而派生出高效的程序。通过这种方式，Fiat使得将程序分为功能和性能两个部分成为可能，并强有力地保证了性能部分的错误永远不会违反功能部分的要求。智力上的优点是在模块化程序结构中广泛应用的新思想，具有很强的正确性的形式保证。项目更广泛的意义和重要性是基于在各种各样的环境中显著提高程序员生产力的潜力；该项目还研究了如何将规范的大部分自动化改进的想法集成到入门编程和离散数学课程中，以充分说明逻辑符号在编程中的价值。项目中的主要案例研究领域是实用的Internet服务器，例如用于域名查找或电子邮件传递的服务器。目标是开发这些关键服务的Fiat版本，自动生成高效的可执行代码。过去从SQL风格的规范中派生数据层的工作正在得到扩展，此外还在探索规范和自动派生的其他领域，例如从语法中合成解析器，用于服务器所说的协议，它们读取的配置文件等。除了研究如何构建和组合这样的新库之外，该项目还研究了如何将合成过程推进到比我们的原型实现更低的抽象级别，从而生成功能程序。改进后的Fiat系统将派生装配程序，通过对机器资源的更直接控制，实现更有效的优化选择，并与Bedrock Coq库集成，实现经过验证的多语言编程。