Class 4: Curry-Howard

For this class, we are going to take a look at explicit proof objects by way of an exercise in Agda. Agda is a great proof assistant for looking at proof objects because it's deliberately minimalistic when it comes to automation.

It is because of this minimalism that, to write proofs in Agda, you really have to understand how proof objects work. And in my experience, having a strong grasp of proof objects makes it much easier to build proof automation of all kinds---from the traditional proof automation we'll see next week, all the way to the neural networks we'll see in later classes. This is why we're starting in Agda and building up from there.

Installation can be finicky, so please install the artifact before class using the instructions below. If you have any trouble, please post your questions in this thread. You can also drop any installation tips you have in that thread.

Slides from this class are here, and solutions have been posted in the class forum.

Installation Instructions

New this year, thanks to our wonderful TA Vasista Vovveti, there is a cloud based environment for this artifact available here. If you would like to use the cloud based environment, please familiarize yourself with it before class.

Otherwise, to install from source:

1. Install Agda from source using cabal or stack by following these instructions. This took me 20 minutes on Ubuntu, with most of that time waiting for Agda 2.6.2.1 to compile.
2. Set up agda-mode for Emacs using these instructions on the same page. This took me a few seconds on Ubuntu, after I resolved some path issues by creating symlinks to the agda and agda-mode binaries from /usr/bin.
3. You are now done setting up Agda. You do not need the standard library for this artifact. (You can install it if you want, but we won't be using it.)
4. To test your Agda setup, download this copy of the hello world file from the instructions.
5. Next, compile the hello world file in Emacs using these instructions. The first time you do this, you will be asked for a backend---type GHC and press enter. (You can alternatively just run Ctrl+C Ctrl+l to load but not compiled the code; this is all you will need to do for proofs in class).
6. Next, run the resulting compiled hello-world file (without the .agda extension). This should print "Hello world!"
7. Download this file---we will hack on this in class! An HTML version is here if you'd like to browse it online.

If installation fails, and the class forums are no help, do not panic; we will try to match you with someone in class for whom installation worked. (I've especially heard that folks with the latest Apple computers have had trouble with this in the past, so please let me know if this is you.)

You can find the exercise we will do together in class below.

During class, we will divide up into groups, pairing up people who already have experience with people who are totally new to this. We will then do the exercise in this file. There is an HTML version of this file here, if you'd like to browse it online. You can do this on your own if you cannot make it to class, or let me know if you'd like me to find you a partner or make an exception.

There is a discussion question at the bottom of the file. This is the only graded part. Please have your group post your answers in this thread, following the directions from the file.