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
Sponsors
This episode is sponsored by DailyDrip.com. Use the coupon `geekery` to save $9 on your first month, and make learning part of your daily routine with DailyDrip.com.
Announcements
f(by) is coming up on the 10th of December in Minsk, Belarus. Visit http://fby.by to find out more and to register.
Lambda Days will be taking place again on the 9th and 10th of February 2017. Visit www.lambdadays.org 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 http://www.katsconf.com/ to register and for more information.
ClojureD will be taking place on the 25th of February, 2017, in Berlin, Germany. Visit www.clojured.de 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 www.bobkonf.de for more information about the conference.
Destination Code, a new unconference starting in Utah, is having its inaugural event March 27-30th, 2017. Visit http://www.destination.codes/ to find out more.
Erlang & Elixir Factory 2017 is on the 23rd and 24th of March. Visit www.erlang-factory.com/sfbay2017 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 http://2017.flatmap.no/cfp/ to learn more.
If you have a conference related to functional programming, contact me, and I will be happy to announce it.
Topics
About Jared
Lean Theorem Prover
How Jared got into software development
How Jared was first exposed to functional programming
Haskell
Scala
Clojure
Ruby
How learning functional programming affected daily work in Ruby and Rails
What captured Jared’s interest in typed languages
Rust
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
Idris
Verified pacemaker on functional architecture chip
FPGA – Field-programmable gate array
Jared’s introduction to dependent types
Software Foundations
Certified Programming with Dependent Types
Coq
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
Nuprl
JonPRL
F*
Lean
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
Dafny
Project Everest
As always, a giant Thank You goes to David Belcher for the logo design.
*** Update January 18th ***
Typed Coin