Abstractification

Large language models can rapidly generate and modify programs for a given specification, leading to a verification bottleneck in the software development cycle. We present abstractification, a programming model using program sketching that separates the specification of a program from its implementation, requiring human review only at specification boundaries. Abstractified programs contain holes that a model is free to change, mechanically derived or human-authored verifiers that evaluate any proposals to the holes, and the surrounding program that is part of the specification. We propose an autonomous optimization agent that can use manually written benchmarks, performance fuzzing and recorded inputs for optimization by autonomously searching through optimized candidates for holes in a program in a CEGIS-style program synthesis loop. We prototype abstractification in Rust using macro annotations for reference implementations, contracts, data models, and optimization objectives. Our preliminary study of allocation heuristics in Rust's str::replacen illustrates that the best implementation choice can significantly depend on the production workload, and that the hole-oriented approach can allow for the model to autonomously search for optimizations without per-proposal human review within the explicitly defined search space.