Certainty by Construction Progress Report 2
The following is a progress report for Certainty by Construction, a new book I’m writing on learning and effectively wielding Agda. Writing a book is a tedious and demoralizing process, so if this is the sort of thing you’re excited about, please do let me know!
It’s week two of regular updates on Certainty by Construction, baby! This week I made 17 commits to the repository, half of which were towards the goal of improving the book’s typesetting. Spurred on by a bug report asking “what the hell does AgdaCmd:MakeCase mean?” I decided to upgrade the book’s build system. Now you should see explicit keystrokes to press when the book asks you to run a command alongside.
You’ll also notice intra-prose syntax highlighting, meaning that if the book mentions a type, it will now be presented in a beautiful blue, among other things in other colors. Agda has some janky support for this, but I couldn’t get it working, which means I annotated each and every piece of syntax highlighting by hand. Please file a bug if you notice I’ve missed any.
Content-wise, the old chapter on “structured sets” has become “relations”, and it has several new sections fleshing out the idea and giving several more examples. I’m now in the middle of rewriting the setoids chapter, but it too has three new sections, and thus the whole thing is no longer all about modular arithmetic.
Next week I’m going to continue powering on with the setoids chapter—including a big digression on what congruence entails under a setoid—and then I think I’ll tackle the ring solving chapter.
For the first time, this book seems like I might not be working on it for the rest of my life. It’s nowhere near done, but the topic and style are finally hashed out, and the content is mostly in an alpha state. From here it’s really just to continue grinding, rewriting all the crap bits over and over again, until they’re no longer crap.
Anyway, that’s all for today. If you’ve already bought the book, you can get the updates for free on Leanpub. If you haven’t, might I suggest doing so? Your early support and feedback helps inspire me and ensure the book is as good as it can possibly be.