[Haskell'22] Reasonable Agda is Correct Haskell: Writing Verified Haskell using agda2hs

Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs (Video, Haskell 2022)
Jesper Cockx, Orestis Melkonian, Lucas Escot, James Chapman, and Ulf Norell
(Delft University of Technology, Netherlands; University of Edinburgh, UK / Input Output, UK; Delft University of Technology, Netherlands; Input Output, UK; University of Gothenburg, Sweden)

Abstract: Modern dependently typed languages such as Agda can be used to
statically enforce the correctness of programs. However, they still
lack the large ecosystem of a more popular language like Haskell.
To combine the strength of both approaches, we present agda2hs, a
tool that translates an expressive subset of Agda to readable
Haskell, erasing dependent types and proofs in the process.
Thanks to Agda's support for erasure annotations, this
process is both safe and transparent to the user.
Compared to other tools for program extraction, agda2hs uses a syntax
that is already familiar to functional programmers, allows for both
intrinsic and extrinsic approaches to verification, and produces
Haskell code that is easy to read and audit by programmers with no
knowledge of Agda.


We present a practical use case of agda2hs at IOG
to verify properties of a program generator.
While both agda2hs and its ecosystem are still young, our
experiences so far show that this is a viable approach to make
verified functional programming available to a broader audience.


This paper is a literate Agda script, hence all rendered (Agda) code has been typechecked.

Article: https://doi.org/10.1145/3546189.3549920

ORCID: https://orcid.org/0000-0003-3862-4073, https://orcid.org/0000-0003-2182-2698, https://orcid.org/0000-0001-9642-5641, https://orcid.org/0000-0001-9036-8252, https://orcid.org/0000-0003-2999-0637

Video Tags: Dependent types, Agda, Formal verification, Program extraction, icfpws22haskellmain-p50-p, doi:10.1145/3546189.3549920, orcid:0000-0003-3862-4073, orcid:0000-0003-2182-2698, orcid:0000-0001-9642-5641, orcid:0000-0001-9036-8252, orcid:0000-0003-2999-0637

Presentation at the Haskell 2022 conference, September 15–16, 2022, https://icfp22.sigplan.org/home/haske...
Sponsored by ACM, ACM SIGPLAN, https://www.sigplan.org/