An approach to translating Haskell programs to Agda and reasoning about them

TL;DR

This paper presents a library that facilitates translating Haskell programs to Agda, enabling formal verification and reasoning about the correctness of complex distributed systems like Byzantine Fault Tolerant consensus algorithms.

Contribution

The authors developed an open-source library that closely mirrors Haskell code in Agda, simplifying translation, review, and maintenance for formal verification purposes.

Findings

Library enables accurate Haskell-to-Agda translation

Facilitates formal reasoning about translated programs

Reduces translation errors and maintenance effort

Abstract

We are using the Agda programming language and proof assistant to formally verify the correctness of a Byzantine Fault Tolerant consensus implementation based on HotStuff / LibraBFT. The Agda implementation is a translation of our Haskell implementation based on LibraBFT. This short paper focuses on one aspect of this work. We have developed a library that enables the translated Agda implementation to closely mirror the Haskell code on which it is based. This makes it easier and more efficient to review the translation for accuracy, and to maintain the translated Agda code when the Haskell code changes, thereby reducing the risk of translation errors. We also explain how we capture the semantics of the syntactic features provided by our library, thus enabling formal reasoning about programs that use them; details of how we reason about the resulting Agda implementation will be presented in a future paper. The library that we present is independent of our particular verification project, and is available, open-source, for others to use and extend.