一句话：提出首个面向安全 Rust 的按构造正确程序合成方法，用 Synthetic Ownership Logic 将类型约束与功能规约结合。
Rust 类型系统虽保证内存安全与无数据竞争，但其严格规则使许多惯用实现模式需大幅改写，增加手工编程负担。本文指出自动合成反而可受益于 Rust 类型：类型可推断数据结构形状、别名与效果，从而简化规约；类型约束还能缩小搜索空间。作者提出首个在 safe Rust 中自动合成构造正确程序的方法，核心是 Synthetic Ownership Logic，一种保证程序同时满足用户功能规约与 Rust 类型系统的新型程序逻辑，并实现工具 RusSOL。评估表明 RusSOL 在标注负担与性能上均有效，能为 Rust 新手常见问题合成可证明正确的解。
The Rust type system guarantees memory safety and data-race freedom. However, to satisfy Rust's type rules, many familiar implementation patterns must be adapted substantially. These necessary adaptations complicate programming and might hinder language adoption. In this paper, we demonstrate that, in contrast to manual programming, automatic synthesis is not complicated by Rust's type system, but rather benefits in two major ways. First, a Rust synthesizer can get away with significantly simpler specifications. While in more traditional imperative languages, synthesizers often require lengthy annotations in a complex logic to describe the shape of data structures, aliasing, and potential side effects, in Rust, all this information can be inferred from the types, letting the user focus on specifying functional properties using a slight extension of Rust expressions. Second, the Rust type system reduces the search space for synthesis, which improves performance. In this work, we present the first approach to automatically synthesizing correct-by-construction programs in safe Rust. The key ingredient of our synthesis procedure is Synthetic Ownership Logic, a new program logic for deriving programs that are guaranteed to satisfy both a user-provided functional specification and, importantly, Rust's intricate type system. We implement this logic in a new tool called RusSOL. Our evaluation shows the effectiveness of RusSOL, both in terms of annotation burden and performance, in synthesizing provably correct solutions to common problems faced by new Rust developers.
@article{paperbot2001,
title = {Leveraging Rust Types for Program Synthesis},
author = {Jonáš Fiala and Shachar Itzhaky and Peter Müller and Nadia Polikarpova and Ilya Sergey},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591278}
}