This summer I’m working intensely with a few students on disco, a functional teaching language for discrete mathematics I’ve been developing. We’re working mostly on type-theoretic foundations for the language and filling out its set of implemented features. So far we have refactored the codebase to use techniques from “Trees that Grow” by Najd and Peyton Jones, and are working on adding polymorphism to the type system as well as adding a built-in set type.
Lately I’ve been solving more problems on Open Kattis, for fun and as preparation for coaching the Hendrix programming team.
Chris Chalmers has been working on an rewrite of some of the core functionality of the diagrams library, which will allow for things like traversals over diagrams and diagram edits; get rid of the backend type parameter for diagrams (which was more of a nuisance than a help); and incidentally split out all the purely geometric parts of the library into a separate package. I’m excited to see this land (hopefully over the summer) and am helping with feedback, documentation, and so on.
I’m in the middle of a series of blog posts on The Math Less Traveled exploring primality testing algorithms. I’ve finished up a sub-series exploring proofs of Fermat’s Little Theorem; next up is to start writing about primality tests themselves, and why it seems (but we can’t prove) that we live in a rather interesting universe where primality testing can be done quickly but not factoring.
However, the above series is on hold while I explore another rabbit hole: I recently figured out how to use an SMT solver to create minimal drawings of orthogons (polygons with only right angles), and am writing up some blog posts to explain it. Here’s the latest post in the series.
…but the above series is itself on hold while I write about the recent progress on the Hadwiger-Nelson problem. Hopefully by the end of the summer I can pop the stack and finish up all these series.
The semester is over! This summer I’ll be preparing to teach several classes in the fall:
- CSCI 150, Foundations of CS
- CSCI 382, Algorithms
- CSCI 360, Programming Languages
Things I’m reading right now:
- An Illustrated Theory of Numbers by Martin Weissman (I recently published a review on my blog)
- Grace Hopper and the Invention of the Information Age by Kurt W. Beyer
- I am reading the book of Genesis in the original Hebrew, a little bit every day; currently in chapter 13.