Functional Geekery Episode 71 – Nikhil Swamy

In this episode I talk with Nikhil Swamy. We talk F*, dependent types, proving software, Dijkstra Monads, Project Everest for verified HTTPS, and more.

Our Guest, Nikhil Swamy

Nikhil Swamy


CodeMesh is taking place the 3rd and 4th of November with tutorials on the 2nd of November. Tickets are available now, but they are going fast. Visit to register and submit your talk.

Scala Wave is coming up on the 25th and 26th of November in Gdańsk, Poland. Visit to find out more and sign up for their newsletter for updates.

Destination Code, a new unconference starting in Utah, is having its inaugural event this December. Visit to find out more.

The 2016 Clojure Conj will be taking place in Austin, TX on December 1st – 3rd. Visit for more information 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.

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

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


About Nik
Microsoft Research Labs
How Nik got into proving software
F* as a combination of interactive and automated proofs
SMT Solvers
Dependent Types and Dependent Type systems as provers
Embracing Effects in F*
Using Type Systems to prove things about your program
Expressing a list as sorted using Dependent Types
Types as Sets
Testing is a means try to disprove your program
Dependent Types as a means to verify your program
Typed Lambda Calculus
Proving that a list is sorted
Hints and Lemmas
Curry-Howard Isomorphism
F* Tutorial
F* Quicksort Tutorial Example
POPL 2017
Dijkstra Monads for Free
Weakest Pre-condition of a program
Weakest Pre-condition adapted to monads
Improvement of tooling for proving software in the past 10 years
Project Everest
Build and deploy verified drop in replacement for HTTPS stack
TLS – Transport Layer Security
Writing programs at the Assembly level and proving them correct
Z3 Theorem Prover
F* being used to prove Project Everest’s correctness
Euro Security and Privacy
F* on Github
F* Slack channel
F* mailing list
“Specify before proving”
“Try to specify before even writing a line of code”
F* for the Masses blog

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

One thought on “Functional Geekery Episode 71 – Nikhil Swamy

  1. Jacob Zimmerman

    I’m unable to download this easily, especially on my phone.
    Clicking the download button just opens a player in the browser. On a desktop, I can find my way to downloading it at that point, but not on my phone, where I want to download it to.
    Also, the download button is a true button, and therefore doesn’t provide the right-click option to save/download what the link points to.
    Lastly, I only use a simple RSS feed reader, not one designed for podcasts, so that gives me nothing as well.


Leave a Reply

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