2025/09/26 by Zhao, Jianhong, Hildenbrandt, Everett, Conejero, Juan +1
#Computation and Language (cs.CL) #FOS: Computer and information sciences #Programming Languages (cs.PL)
paper · doi:10.48550/arxiv.2509.21793
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.