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
F*

Announcements

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 codemesh.io to register and submit your talk.

Scala Wave is coming up on the 25th and 26th of November in Gdańsk, Poland. Visit http://www.scalawave.io/ 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 http://www.destination.codes/ to find out more.

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

ClojureD will be taking place on the 25th of February, 2017, in Berlin, Germany. Visit www.clojured.de 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.

Topics

About Nik
Microsoft Research Labs
F*
How Nik got into proving software
Coq
Agda
Cyclone
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
Idris
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
Lean
Typed Lambda Calculus
Proving that a list is sorted
Quicksort
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
Inria
Build and deploy verified drop in replacement for HTTPS stack
HTTPS
TLS – Transport Layer Security
OpenSSL
Heartbleed
X.509
Spartan
Writing programs at the Assembly level and proving them correct
Dafny
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.

Episode source