Erlang is an unorthodox language because fault-tolerance and observability (tracing) are baked into the language. This allows users to debug production systems without the maintenance overhead of adding these features manually, but comes at the cost of adding a side effect to almost every operation.

Because of tracing, the compiler does not have much freedom to perform common optimizations, and requires sophisticated analysis to safely apply all but the simplest transformations. Each individual optimization also implements its own bespoke analysis, which is error-prone and difficult to maintain.

This report describes an ongoing experiment on translating one of the compiler’s intermediate representations (IR) to formulas, enabling the use of a satisfiability modulo theories (SMT) solver to drive analysis as well as prove the semantics-preserving nature of optimizations.