You got Agda in my Haskell? By Ryan Orendorff

One of your coworkers seems to write the most amazing Haskell code. It never breaks and it always fits the requirements precisely. You’ve never seen your coworker put in a bug fix for their code ever. One day you decide to ask them how they obtained these inhuman powers. With a huge grin on their face, they say “why that’s because I wrote all my provably correct code in Agda!”

In this talk, we will talk about a new tool called agda2hs which allows programmers to translate dependently typed Agda code into clean Haskell code, enabling the extraction of provably correct programs. We will look into specific examples on how the code can be used to prove that a piece of code has some desired specification such as invertibility.

About our speaker

Hi! My name is Ryan Orendorff, and I enjoy working on type theory, functional programming, linear algebra, and data privacy. If I am not working on those things you can likely find me on a mountain somewhere.

Personal page and Blog: Ryan Orendorff

Event details: https://www.meetup.com/bay-area-haskell-user-group/events/290844236/

This Recording is also available on YouTube