Embracing a mechanized formalization gap

TL;DR

This paper explores a method to simplify complex code verification by intentionally introducing a formalization gap, demonstrated through translating parts of GHC into Coq for invariant verification.

Contribution

It presents a novel approach to manage verification complexity by deliberately creating a formalization gap, enabling verification of large codebases.

Findings

Successfully translated core GHC components into Coq

Verified invariants related to term variable usage

Demonstrated the practicality of the formalization gap approach

Abstract

If a code base is so big and complicated that complete mechanical verification is intractable, can we still apply and benefit from verification methods? We show that by allowing a deliberate mechanized formalization gap we can shrink and simplify the model until it is manageable, while still retaining a meaningful, declaratively documented connection to the original, unmodified source code. Concretely, we translate core parts of the Haskell compiler GHC into Coq, using hs-to-coq, and verify invariants related to the use of term variables.