From testing to formal verification in Haskell

Abstract

Haskell’s expressive type-system saves developers from writing several categories of bugs. Yet, even though it allows them to encode complicated invariants statically, logic related errors can still escape to the type system. Typical testing mechanisms are still offered to ensure higher levels of quality of pieces of software written in Haskell. In particular, the testing framework QuickCheck6 enables a type-based property testing, where the programmer encodes invariants as properties, and the library generates (appropriate) test data to cover them. It is a known issue that the effectiveness of any testing mechanism is sensitive to the nature of the test cases and formal verification is preferred whenever applicable. LiquidHaskell allows enhancements to the Haskell’s type-system with refinement types in order for developers to encode type-based invariants and automatically prove their satisfiability using an SMT solver. Typically, trivial properties are easily proved by LiquidHaskell, whereas other times the developer needs to manually provide inductive hypotheses, additional lemmas, or use equational reasoning to complete the proof. In this thesis work we study the ”manual” proofs in LiquidHaskell. We formally prove QuickCheck properties of a real-world library and study a way to automate a major part of the manual work. We introduce a proof generator written in Template Haskell21 that, given a boolean property (QuickCheck test), automatically generates the corresponding proof to formally verify the property in LiquidHaskell. We noticed that many of the manual proofs involve induction and case splitting, thus, we integrated into the proof generator two heuristics that help in those cases in a similar style to the tactics in Coq 4 proofs.