Formal Education: Self-Study with Coq and ChatGPT
There are many different tools available to verify whether or not a system will run correctly. While mostly I’ve explored model checkers, I’ve long had my eye on Coq, which is a theorem prover. Basically, Coq is an assistant to prove mathematical properties. Along with Isabelle and a few others, Coq is the gold standard for this kind of work.
One thing that sets Coq apart is the literature around it. Benjamin Pierce, a professor at the University of Penn and a leading programming language researcher, has developed Software Foundations. Currently a 6-volume series, the material covers about two or three graduate-level courses. The first two books are the basis for a class introducing programming language theory to advanced undergraduate and graduate students. Cornell professor Michael Ryan Clarkson has a YouTube Playlist going through this course, and there are also video lectures with Pierce from the Oregon Programming Languages Summer School.
In Ultralearning, the brand of self-education evangelized by Scott Young in his blog and book, the key to actual learning is identified as doing exercises, as well as what’s described as “relentless experimentation”. Malcolm Gladwell’s notorious 10,000 hours notes that it’s not just doing exercises, but doing the exercises and receiving expert feedback which really leads to improvement. This is something where computer programming excels. I can learn a language like F# and go to Exercism to work through over a hundred questions. There are other websites that offer code wars, programming katas and dozens of other variations on programming.
Software Foundations is completely verified in Coq, which means that each chapter can be run inside of Coq. There are exercises left to the reader which Coq is able to then check for accuracy. Finally, there is an included auto-grader. I had to whip up a small Python script to track how many points I was earning out of the total, but suffice to say if you do all the exercises, you’ll get an A.
Self-study is hard. It’s hard to stay motivated. It’s really hard to figure things out when you’re stuck. While Software Foundations is thorough, there are still some gaps. For example, it wasn’t clear to me what the syntax was for destructing a tuple. Fortunately, ChatGPT has the answers. I was able to put some simple queries into ChatGPT about Coq syntax and get answers like I would from a teaching assistant. I don’t need all the answers, just a little push in the right (especially syntactic) direction.
I haven’t used ChatGPT a lot, but this seems like a great use-case for its educational value. I just listened to an AWS education executive on Corey Quinn’s podcast talk about how this sort of Generative AI can help move the dial with students. It certainly moved the dial with me. Instead of getting frustrated, I got on the road to a solution. First, I asked for a motivational speech — because I’m early in the process and getting stuck and it’s frustrating! Then I asked for a hint for a solution. That’s sort of like going to a Teacher’s Assistant for help on the homework. The next step, I told ChatGPT that we were students together and asked to share a solution. This is like being part of a study group. ChatGPT got the wrong answer, though (this project looks like an interesting way to get the right one), so I had to work through the hints and partial solution to write my own solution. I then shared it with ChatGPT for some feedback (TA again). Overall, I was able to gain confidence that I had answered the question in the right way, and that I wasn’t off track. I was also able to fill in some gaps in my understanding by thinking through the problem with new input.
I think it’s important to note that there’s an important combination of resources here that works for me. There’s a free online textbook, video lectures, a set of exercises that are graded, and a chatbot which can provide helpful suggestions. One way to learn is to teach, and part of the process is teaching ChatGPT why it’s wrong. This is pretty close to a classroom experience. It’s similar to another successful model — Coursera, with video lectures, graded questions and a forum where students can share tips or questions. But I’ve gotten stuck on Coursera classes because somethings might be peer-graded, or the explanation doesn’t fully explain what’s expected. Coq is pretty explicit about what it wants, and it’s interactive, so I can see exactly where I am going wrong. Submitting answers to Coursera is a black box — Coq is transparent.
I’m early into the first chapters of Software Foundations. I hope I’ll be able to keep up the motivation to work through at least the first course, which is mostly the first two books. If I get stuck, I can always ask ChatGPT for another pep talk!
