一句话：提出一种介于 C 与 Rust 之间、面向计算机代数底层库的安全低级语言，并用 Coq 证明其安全性及基于 CompCert 的编译器语义保持。
计算机代数系统依赖 GMP、BLAS/LAPACK 等底层库，这些库通常用 C、Fortran 和汇编编写，大量使用数组与指针，安全和演绎验证困难。本文提出一种介于 C 与 Rust 之间的低级语言，专为计算机代数底层库设计，既保持低层效率又便于程序验证。作者基于 CompCert 实现了该语言编译器，并在 Coq 中形式化证明了语言安全性和编译器语义保持性。该语言尚未覆盖所有特性，但展示了设计领域特定语言及其形式验证编译器所需的关键步骤。
This article describes a programming language for writing low-level libraries for computer algebra systems. Such libraries (GMP, BLAS/LAPACK, etc) are usually written in C, Fortran, and Assembly, and make heavy use of arrays and pointers. The proposed language, halfway between C and Rust, is designed to be safe and to ease the deductive verification of programs, while being low-level enough to be suitable for this kind of computationally intensive applications. This article also describes a compiler for this language, based on CompCert. The safety of the language has been formally proved using the Coq proof assistant, and so has the property of semantics preservation for the compiler. While the language is not yet feature-complete, this article shows what it entails to design a new domain-specific programming language along its formally verified compiler.
@article{MelquiondM24,
title = {A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler},
author = {Guillaume Melquiond and Josué Moreau},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674629}
}