Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report)

Abstract

Good tools can bring mechanical verification to programs written in mainstream functional languages. We use <pre>hs-to-coq</pre> to translate significant portions of Haskell’s <pre>containers</pre> library into Coq, and verify it against specifications that we derive from a variety of sources including type class laws, the library’s test suite, and interfaces from Coq’s standard library. Our work shows that it is feasible to verify mature, widely-used, highly optimized, and unmodified Haskell code. We also learn more about the theory of weight-balanced trees, extend <pre>hs-to-coq</pre> to handle partiality, and – since we found no bugs – attest to the superb quality of well-tested functional code.