Certainty by Construction Progress Report 10

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!

---

Thanks for all of your kind words of support after my last report. That’s the sort of thing that really helps keep me motivated. So thank you!

BUT GOOD NEWS. HERE’S SOMETHING ELSE THAT ALSO HELPS TO KEEP ME MOTIVATED.

I just wrapped up the last proof in the book!!!!

It’s taken me all week to put together these glorious 50 lines of Agda, but it makes for a damn fine finale for the book. So the game plan is now to delete that last chapter I’ve got hanging around that’s kinda about matrices, rewrite the prose on isomorphisms, and then do one final polish pass where I add things like indices and definitions.

Grad school has been much busier than I was expecting it to be, but no matter! I will persevere. Being so close to the finish line is tantalizing and I expect I’ll just spend the next few days powering through it all. This thing is definitely going to be finished by the end of the year.