Writing a formally-verified image browser in Coq and Haskell (2017)

Our Haskell code will be using our own custom functions that manipulate these types, which will be formally-verified. Roughly, things that can be extracted into living, breathing computer code lie in Coq’s ; while the world of theorems and proofs is Coq’s . Coq allows us to map inductive types directly to Haskell.

Source: www.michaelburge.us