Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics
Programming Languages
2025-09-29 v1 Computation and Language
Abstract
Verification proofs encode complete program behavior, yet we discard them after checking correctness. We present compiling by proving, a paradigm that transforms these proofs into optimized execution rules. By constructing All-Path Reachability Proofs through symbolic execution and compiling their graph structure, we consolidate many semantic rewrites into single rules while preserving correctness by construction. We implement this as a language-agnostic extension to the K framework. Evaluation demonstrates performance improvements across different compilation scopes: opcode-level optimizations show consistent speedups, while whole-program compilation achieves orders of magnitude greater performance gains.
Cite
@article{arxiv.2509.21793,
title = {Compiling by Proving: Language-Agnostic Automatic Optimization from Formal Semantics},
author = {Jianhong Zhao and Everett Hildenbrandt and Juan Conejero and Yongwang Zhao},
journal= {arXiv preprint arXiv:2509.21793},
year = {2025}
}