For those that wonder what they're seeing, this book is about writing functional programs and proving them correct. This is done in the context of a dependentl

For those that wonder what they're seeing, this book is about writing functional programs and proving them correct. This is done in the context of a dependently-typed language called Coq. An example of a dependent type is having a function that takes an integer value n and an array of size n as arguments and having the type system check that you call the function with a valid size and array at compile-time. It turns out that dependent types can be used in much more powerful ways, including proving deep correctness properties about programs (less powerful type systems (like Java's) are also "proofs", but the correctness properties they check are typically weaker).