Domain-specific languages (DSLs) are prevalent across many application domains. Such languages let developers easily express computations using high-level abstractions that result in performant implementations. To leverage DSLs, however, application developers need to master the DSL’s syntax and manually rewrite existing code. Compilers can aid in this effort, but part of building a compiler requires transpiling code from the source code to the target DSL. Such transpilation is typically done via pattern-matching rules on the source code. Sadly, developing such rules is often a painstaking and error-prone process.

In this paper, we describe our experience in using program synthesis to build code transpilers. To do so, we developed VerTrans, a new framework for building transpilers that transform general-purpose code into DSLs using program synthesis. To use VerTrans, transpiler developers first define the target DSL’s semantics using VerTrans’s specification language, and specify the search space for each input code fragment to be transpiled using VerTrans’s API. VerTrans then leverages program synthesizers and theorem provers to automatically find transpilations expressed in the target DSL that is provably semantic equivalent to the input code. We have used VerTrans to build two DSL transpilers targeting different programming models and application domains. Our results show that the VerTrans-based compilers can translate many benchmarks used in prior work created by specialized implementations, but can be built using orders-of-magnitude fewer lines of code as compared to prior work.