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
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 http://www.bus-conf.org/.
Elixir.LDN will be taking place on August 17th. To help encourage inclusion and diversity 30 Free Scholarship places are available. Visit http://www.elixir.london/ to find out more and register.
Compose Melbourne will be taking place August 28th and 29th. For more information and to register, visit http://www.composeconference.org/2017-melbourne/.
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 http://thestrangeloop.com/.
PWLConf 2017 will be taking place September 28th in St. Louis, MO, before Strange Loop. Visit http://pwlconf.org/ 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 openfsharp.org 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 http://con.racket-lang.org/ 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 http://www.lambda.world/.
CodeMesh is coming up November 8th and 9th in London. For more information, and to keep an eye open for registration, visit http://www.codemesh.io/.
Moonconf will be taking place the 9th-11th of November. For more information visit http://moonconf.org/.
If you have a conference related to functional programming, contact me, and I will be happy to announce it.
Announcements
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 https://www.patreon.com/fngeekery.
Topics [@5:07]
About Adam
Coq
“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
Compilers
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
QuickChick
What using Coq to do your proofs looks like
Proof General
Coq IDE
“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
Bedrock
Kami
Software Foundations by Benjamin Pierce, et. al.
DeepSpec project summer school
What domains where formal proof systems fit well
Heartbleed
Cryptography
Fiat Cryptography
Systematic Synthesis of Elliptic Curve Cryptography Implementations
TLS 1.3 standard draft
Ur
Ur/Web
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
Fiat
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.