So I’m about halfway through this undergraduate theory course: and, honestly, it’s been fun and interesting to do for the most part but at the same time I’d like to get Even Better at teaching the students the material in the most effective and least frustrating way. What I *hate* is explaining things in a way that’s tedious or involves lots of busy work. Nothing good comes from busy work, it just is boring. I don’t mean that practice is the same thing as busy work, mind you, but practice that is dull and doesn’t target the right combination of skills really can just be busy work. You don’t want to have students practicing skills that are only tangential to their performance or their comprehension.

For example, this course traditionally has *a lot* of manipulating DFAs and NFAs in its first half. I’ve tried to cut a decent amount of that out while not taking out so much that they don’t get an intuition for the difference between DFAs and NFAs or the power and limitations of the regular languages. We’ll see, after grading the midterm, if I’ve actually hit that goal well. Another thing this course has that, while ultimately good, is proofs. Lots of proofs, lots of mathematical arguments. The decent percentage of the student base that’s taking this class, though, **has no idea how proofs should look**. That’s not their fault, either, but a failing of general math education, the lack of required advanced math courses for their major, and the fact that until they’re juniors or seniors they really just haven’t had to do any courses that teach proofs and now I get to whack them over the head with what’s-really-a-math-course-but-taught-in-the-CS-department *and* it’s required for their major so they have to take it at some point even without getting a good grounding in the principles first.

So that being said, I’ve been pondering how to actually improve this course when I teach it again next year so that, honestly, students aren’t as easily divided into the maths and the math nots because I really don’t think that’s fair. To this end, I’ve been wondering about how to actual do a course like this in a very theorem prover oriented way. Referencing my feelings about explicit proof terms vs. tactics, I feel like there’s something to be said for taking a bunch of programmers and teaching them how to do proofs by writing programs, showing them the connection between proofs-as-programs and the written proofs that are in the text.

I think it would take a solid week or two of learning Agda (or whatever tool is used, but for purposes of this post assume I’ll choose Agda) and learning how to do proofs in a constructive way. Most of the proofs that we actually do in this course *anyway* are constructive and so I think a formal tool is well-suited to the topic. Things such as DFAs, NFAs, CFGs etc. are all decidable when it comes to accepting a string. Turing machines of course, aren’t necessarily so. On the other hand, it’d be pretty cute to actually use coinduction in order to simulate Turing machine descriptions over an input. We might be able to even do some proofs about them, given that http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.98.2911 gives a notion of a constructive version of the halting problem and a proof that it’s not decideable. Computatable reductions would probably make more sense than when we try to give a pen & paper informal Turing machine description if they can be represented as actual code one manipulates.

In the end, I don’t think I could completely eliminate the use of pen & paper in this undergraduate course but we might be able to wean them onto informal mathematics by using dependently typed programming as a bridge. The question, of course, is if dependently typed programming would be even more confusing for students to learn than just pen & paper proofs! I fully accept that this might be the case and the whole thing just might end up being a damn mess. That’s why I’ll see if I can figure out this approach over the next few months and maybe get some feedback from ~~victims~~ friends who might want to also learn a bit about constructive logic.

Oh, this reminds me, I’ve been accepted to give a talk at OS Bridge that will basically be a condensed version of the course I’m currently teaching except only an hour long, with slides, and with me being my normally weird self instead of the rather censored version of myself I present in class.

IMO, one of the big benefits of using a programming environment for proofs is just to show how formal “proofs” are just a fancy name for terms of (generalized) algebraic data types. Working with a literal ADT helps a lot in clarifying how you’re allowed to combine proofs to make larger ones and how you can/cannot thread things through them. This is also one of the reasons I prefer introducing everything via natural deduction, rather than sequent calculus or Fitch-style proofs. A lot of these benefits can be demonstrated just by using GADTs without getting into full-blown dependent types (e.g., in GHC Haskell).

The problem with this approach, however, is that unless your students are already at least passingly familiar with functional programming, you’ll have to teach the basics of FP alongside the proof theory. That’s not a bad thing if the course was all about proof theory; but for an automata theory course, that’s getting a bit off track.