Advertising Coq: Proving is Programming

This repo contains the code, notes and other resources for a presentation that advertises the Coq programming language:

The slides:

• Are shared here: https://slides.com/awalterschulze/advertising-coq
• They contain all the speech as text
• They also contain links to the code that is shared here, which also contain the speech during the demo as comments

Creating these slides included watching a few videos and a brainstorming session, during which notes were taken, see Notes

The code:

1. deMorgenBool.v
2. Sum.v
3. CurryHoward.v
4. Book.v
5. deMorgenProp.v (optional)

The code compiles with Coq version 8.12.0

This presentation was given at:

• Center for Experimental Mathematics, Stellenbosch University on 9 September 2020