Saturday, 28th January, Online Meetup

This meetup was organised by Bay Area Haskell in January 2023


This event listing is provided here for the convenience of Skills Matter Rust community. Please check the organiser's external site for the most up-to-date information.

Please RSVP on

This edition of Bay Area Haskell will feature Ryan Orendorff discussing, "Who got some Agda in my Haskell?"

Once you RSVP you will see the link to twitch to join! For the hallway track and to ask the speakers question you can use the chat on Twitch or join our Channel on Matrix. Any questions about the event please ask in our channel on Matrix. Thank you.

Agenda (Pacific Time)

10.00am - Welcome to SF Haskell by Salar Rahmanian 10.10am - Who got some Agda in my Haskell? By Ryan Orendorff

Who Got Some Agda in My Haskell?

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.

Ryan Orendorff

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.