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

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

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.