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

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