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 ChlipalaAdam’s home pageConference AnnouncementsBusConf 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.AnnouncementsSome 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 canfind out more at https://www.patreon.com/fngeekery.Topics [@About AdamCoq“Theorem proving is a secret weapon for improving the way we build systems”Adam’s first encounter with MLGoing from ML to CoqWhat theorem proving looks like todayAddictiveness of proving softwareXavier Leroy – creator of OCamlGood domains of software for proof assistantsCompilersOverall technology of effective proofsInterfaces between componentsThe Science of Deep Specification@deep_spec on TwitterProving at the internal layers of a systemGenerative Testing compared to Proof SpecificationsQuickChickWhat using Coq to do your proofs looks likeProof GeneralCoq 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 systemsBedrockKamiSoftware Foundations by Benjamin Pierce, et. al.DeepSpec project summer schoolWhat domains where formal proof systems fit wellHeartbleedCryptographyFiat CryptographySystematic Synthesis of Elliptic Curve Cryptography ImplementationsTLS 1.3 standard draftUrUr/WebTier-less languagesHow Ur/Web works at a high levelAutomatically compiling Ur to Server code, Client code, or SQL depending on context of usageSelling points of Ur/Web for Haskell or ML fansObject Capability DisciplineThe Ur/Web People OrganizerHow Higher-Kinded Types fit in Ur/WebUr/Web’s concurrency modelTechEmpower Web Framework BenchmarksImportance of database transactions and their usage in Ur/WebAutomatic retry of transaction failure built into Ur/WebFiatBuilding a DNS server using FiatThe End of History? Using a Proof Assistant to Replace Language Design with Library DesignSNAPL 2017As always, a giant Thank You goes to David Belcher for the logo design.