In this episode Jesper Cockx, one of the main Agda developers, is interviews by Niki Vazou and Matthias Pall. They talk about how to explain dependent types to one’s father, how Agda’s automation and proof search work, and how Agda can be used to verify Haskell code bases.
We are also looking for volunteers:
Are you listening to every of our episodes anyways, and can’t wait for the next one? We could use a dedicated QA listener who gets to listen to each episodes right before it is published, to check for any egregious editing mishaps.
Also, we provide transcripts for each episodes (did you know that?). We get a rough automatically generated transcript out of the recording setup, but it needs to be polished a bit, and we could use more hands who help with that once in a while.
If you’d like to help, please contact us at <email@example.com>.