Functional Geekery Episode 101 – Adam Chlipala

In this episode I talk with Adam Chlipala. We talk Coq, proof assistants, getting started, tooling, domains for advancement using proofs, Ur/Web, and much, much more.

Our Guest, Adam Chlipala

Adam’s home page

Conference Announcements

BusConf will be taking place the 3rd-5th of August in Frankfurt, Germany. Registration is open, and more information can be found at

Elixir.LDN will be taking place on August 17th. To help encourage inclusion and diversity 30 Free Scholarship places are available. Visit to find out more and register.

Compose Melbourne will be taking place August 28th and 29th. For more information and to register, visit

The Strange Loop coming! It will be held in St. Louis, MO on September 28-30, 2017 at the Peabody Opera House. To submit your CfP, visit

PWLConf 2017 will be taking place September 28th in St. Louis, MO, before Strange Loop. Visit for more information and to stay updated on latest announcements.

Open FSharp will be taking place the 28th-29th of September in San Francisco, California. Visit for more information and to register.

RacketCon is October 7th & 8th at the University of Washington, with keynote speakers Dan Friedman and Will Byrd. Visit for more information and to register.

LambdaWorld will be taking place in Cadiz, Spain on October 26th and 27th. For more information visit and to keep updated visit

CodeMesh is coming up November 8th and 9th in London. For more information, and to keep an eye open for registration, visit

Moonconf will be taking place the 9th-11th of November. For more information visit

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


Some of you have asked how you can support Functional Geekery, in that vein,
Functional Geekery now has a Patreon Page.

If that is one of the ways you would like to show your support, you can
find out more at

Topics [@5:07]

About Adam
“Theorem proving is a secret weapon for improving the way we build systems”
Adam’s first encounter with ML
Going from ML to Coq
What theorem proving looks like today
Addictiveness of proving software
Xavier Leroy – creator of OCaml
Good domains of software for proof assistants
Overall technology of effective proofs
Interfaces between components
The Science of Deep Specification
@deep_spec on Twitter
Proving at the internal layers of a system
Generative Testing compared to Proof Specifications
What using Coq to do your proofs looks like
Proof General
“We should be able to take all the mental effort going into unit testing and put it into specifying and proving instead, for at least some important classes of systems.”
How to start moving toward adopting proof systems
Software Foundations by Benjamin Pierce, et. al.
DeepSpec project summer school
What domains where formal proof systems fit well
Fiat Cryptography
Systematic Synthesis of Elliptic Curve Cryptography Implementations
TLS 1.3 standard draft
Tier-less languages
How Ur/Web works at a high level
Automatically compiling Ur to Server code, Client code, or SQL depending on context of usage
Selling points of Ur/Web for Haskell or ML fans
Object Capability Discipline
The Ur/Web People Organizer
How Higher-Kinded Types fit in Ur/Web
Ur/Web’s concurrency model
TechEmpower Web Framework Benchmarks
Importance of database transactions and their usage in Ur/Web
Automatic retry of transaction failure built into Ur/Web
Building a DNS server using Fiat
The End of History? Using a Proof Assistant to Replace Language Design with Library Design
SNAPL 2017

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

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.