Functional Geekery Episode 77 – Jared Roesch

In this episode I talk with Jared Roesch. We talk his history of functional programming, work on the Rust compiler, dependent types, the Lean Proving Language, and much, much more.

Our Guest, Jared Roesch

@roeschinc on Twitter
jroesch on Github


This episode is sponsored by Use the coupon `geekery` to save $9 on your first month, and make learning part of your daily routine with


f(by) is coming up on the 10th of December in Minsk, Belarus. Visit to find out more and to register.

Lambda Days will be taking place again on the 9th and 10th of February 2017. Visit to submit your talk and keep updated as more information becomes available.

Kats Conf 2 will be taking place in Dublin, Ireland on the 18th of February. Visit to register and for more information.

ClojureD will be taking place on the 25th of February, 2017, in Berlin, Germany. Visit to get tickets and keep updated as more information becomes available.

BOB Konf is taking place the 24th of February 2017 in Berlin, Germany. Visit for more information about the conference.

Destination Code, a new unconference starting in Utah, is having its inaugural event March 27-30th, 2017. Visit to find out more.

Erlang & Elixir Factory 2017 is on the 23rd and 24th of March. Visit for more information.

flatMap(Oslo) is a FP-conference with focus on Scala and the JVM, taking place on May 2nd and 3rd in Oslo, Norway. Please go to to learn more.

If you have a conference related to functional programming, contact me, and I will be happy to announce it.


About Jared
Lean Theorem Prover
How Jared got into software development
How Jared was first exposed to functional programming
How learning functional programming affected daily work in Ruby and Rails
What captured Jared’s interest in typed languages
POPL – Principles of Programming Languages
Jared’s work with Rust
Rust’s ability to support functional programming concepts
“A love child between Haskell and C++”
Rust’s support for scoped mutation of data
Type classes and traits in Rust
ASPLOS – Architectural Support for Programming Languages and Operating Systems
Verified pacemaker on functional architecture chip
FPGA – Field-programmable gate array
Jared’s introduction to dependent types
Software Foundations
Certified Programming with Dependent Types
General lack of tooling for getting started in dependent type languages
Type-driven Development with Idris
Formal Reasoning About Programs
Intrinsic vs extrinsic proofs with dependent types
Dependent types and their relation, or not, to functional programming
The goal of making dependent types accessible with Lean
Z3 SMT solver
The 30,000 foot view and philosophy of Lean
Scripting Lean in Lean
Theorem Proving in Lean
eBPF – Extended Berkeley Packet Filter
Provable eBPF compilation
Target of Lean
Project Everest

As always, a giant Thank You goes to David Belcher for the logo design.

*** Update January 18th ***
Typed Coin

Leave a Reply

Your email address will not be published. Required fields are marked *

This site uses Akismet to reduce spam. Learn how your comment data is processed.