“Certainty by Construction” is a book revolving around Agda that is written by the “Thinking with Types” and “Algebra-Driven Design” author-- Sandy Maguire, here is the link:
P.S: Am not Sandy Maguire, I wanted to share the book if anybody is interested.
Nice, but what does this have to do with Haskell?
From the author: “Certainty by Construction is a book on doing mathematics and software design in the proof assistant Agda, which is the language Haskell wants to be when it grows up.”
Many Agda ideas contaminate and will contaminate Haskell, many haskellers are interested in type theory beyond what Haskell2010 offers.
Agda is also written in Haskell and has similar syntax so some people in the Haskell community use Agda to prove properties of Haskell code using agda2hs.
[…] the proof assistant Agda, which is the language Haskell wants to be when it grows up.
Does the book have one or more chapters dedicated to using Agda for implementing Agda? (something which Haskell has been doing since 1989…)