Talk by Stephan Boyer at the Bay Area Haskell Users Group (BAHUG) meetup at Formation, December 11 2018.

Have you ever wanted to formally prove an algorithm correct or a theorem true? This talk will show you how! We'll cover the fundamentals of computer-assisted theorem proving using Coq, one of the most popular proof assistants. Coq is a functional programming language whose type system can encode essentially any mathematical proposition.

Most introductions to Coq survey the landscape from a bird's eye view. You start by building proof scripts using high-level "tactics", and later you're introduced to the actual proofs generated by these tactics. For some, this is a bit too magical. You learn to prove simple theorems, but lack intuition for what the tactics are actually doing. That conundrum was frustrating for me when I was learning Coq in graduate school. This talk, in contrast, will feature no magic.

Instead, we will approach Coq from the perspective of a functional programmer. We'll start with the syntax, which will be familiar to Haskell programmers. We'll learn how to encode propositional logic in data types, which can be done in any functional language. Then we'll see how to encode quantifiers using dependent types, which completes the foundation of higher-order logic. Finally, we'll learn how to automate our proofs using Coq's tactic language. The more you automate, the shorter and more robust your proofs become!

Also available on YouTube: https://youtu.be/bCxqtD-jH48