An introduction to formal proof verification and the Curry-Howard Correspondence

Contents The Curry-Howard correspondence How do proof assistants use the CH correspondence A theorem A proof of the theorem The type checker Limitations of the type checker Mathematical consequences (and proof) Your type checker maybe wrong Conclusion When writing code many of us have been saved time and time again by type checkers: the useful piece of software that ensures you aren’t adding a string to an integer 1 or returning a reference to a value instead of the owned value. However, while u