# Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code

## TL;DR

This paper demonstrates the feasibility of verifying real-world Haskell code by translating parts of its library into Coq using hs-to-coq, and verifying it against derived specifications, highlighting the potential for formal verification in mainstream functional programming.

## Contribution

It applies hs-to-coq to verify mature Haskell code, extends the tool for partiality, and provides insights into weight-balanced trees and code quality.

## Key findings

- Successful verification of Haskell's containers library
- Extension of hs-to-coq to handle partial functions
- No bugs found in the verified code, indicating high quality

## Abstract

Good tools can bring mechanical verification to programs written in mainstream functional languages. We use hs-to-coq to translate significant portions of Haskell's containers 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 hs-to-coq to handle partiality, and -- since we found no bugs -- attest to the superb quality of well-tested functional code.