In January 2023, I had the great pleasure of welcoming Ryan Orendorff as a speaker to Bay Area Haskell User Group with this awesome talk.
I am making recordings of the meetups I arrange available here on my newsletter first so be sure to subscribe to be the first to view them.
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: https://ryan.orendorff.io/
Event details: https://www.meetup.com/bay-area-haskell-user-group/events/290844236/
For more information about Bay Area Haskell and Functional Programming User Group visit: https://www.sfhaskell.com
You got Agda in my Haskell?