Reasonable Agda is Correct Haskell: Writing Verified Haskell using agda2hs
summary
Tool agda2hs translates an expressive subset of Agda to readable Haskell by erasing dependent types and proofs using Agda's runtime irrelevance (erasure) annotations, producing nearly identical Haskell for examples like a verified BST insert and turning Agda instance-records with erased law proofs into ordinary type classes. The pipeline enforces totality, maps primitives/Prelude, supports error via Absurd→error, and is already used at IOG to verify a program generator and prototype parts of the Cardano codebase; no full formal proof of correctness yet, but practical semantics-preservation checks and constraints prevent leaks.
AI-written summary · about
chapters (12)
- 0:00Agda and agda2hs intro
- 1:50agda2hs design goals
- 3:11Verified binary search trees
- 6:03Agda like Haskell
- 8:50Partial functions safely
- 9:35Type classes in Agda
- 13:47Cardano blockchain use
- 14:53Proofs vs QuickCheck
- 17:03agda2hs implementation
- 18:49Soundness and trusted parts
- 21:19Future work and extensions
- 22:21Demo and events
related talks
49mMaking sense of the Haskell type system
21mProduction Haskell Demystified
59mKeynote: Dependently-Typed Haskell
46mPainless software development with Haskell
01h 22mHaskell for Everyday Programmers
01h 04mHaskell - A Peek Inside the Ivory Tower
01h 07mBuilding a Dependently Typed Language in Haskell Part 1
40mWhat Haskell taught us when we were not looking