The sufficiently smart compiler is a theorem prover

TL;DR

This paper explores how the GHC Haskell compiler's optimizer can serve as a theorem prover to verify code equalities, enabling advanced code validation and optimization techniques.

Contribution

It demonstrates that GHC's simplifier can prove non-trivial equalities, showcasing a novel use of compiler optimization as a formal verification tool.

Findings

GHC's optimizer can prove complex equalities

Implementation of a GHC plugin for equality proofs

Potential applications in verifying library promises

Abstract

That the Haskell Compiler GHC is capable of proving non-trivial equalities between Haskell code, by virtue of its aggressive optimizer, in particular the term rewriting engine in the simplifier. We demonstrate this with a surprising little code in a GHC plugin, explains the knobs we had to turn, discuss the limits of the approach and related applications of the same idea, namely testing that promises from Haskell libraries with domain-specific optimizations hold.