For my birthday, my mom got me the METAFONTbook, 1986 spiral-bound edition.

<3 ​ <3

#typography

💯​ YES. I did it! 100%-ed Software Foundations, Volume 1: Logical Foundations. Every chapter, every single exercise solved.  Some parts were a bit of a slog, as is to be expected, but all in all: Yep, had fun up to the very end. ​

This means, of course, that I should start on Volume 2 (Programming Foundations) soon. I will busy myself with something else this week and possibly next month, but the plan is to get into it by April. Not another 9 year hiatus!

#coq #rocqprover #softwarefoundations

I can now End Pumping. 💪​

This was pretty fun, but phew - lengthy. Proving the (regular) pumping lemma in Coq.

This game (still) rocks.

I binge-completed the first four chapters some time in 2014, did the next four in 2016, and then sadly let the project of finishing "Software Foundations" sit idle for almost ten years. :(

Well, any time is infinitely better than never, so here I go with the significantly expanded 2025 edition!

https://softwarefoundations.cis.upenn.edu/

Image warning: Screenshot spoils the solution to one exercise.

#coq #rocq

This is my first program, bona fide, for the C64! Alas, not written _on_ it which y'all will hopefully excuse, given how the good old boy has neither screen nor keyboard at this time. Also, it's as yet untested, so, probably not correct. :)

#c64 #assembly

And we have a clock. Never mind the ringing, it'll be fine!

Aside from the wonderful jank wiring job, this took me learning how to program the CH32V003. It was a bit of a struggle because I wanted to do it in minimal plain assembly. I had to glean a lot from disassembled C code from ch32fun (which is already a boiled-down environment for it). The official datasheet and reference manual, while not terrible, are lacking in parts and not always written in clear English. I also learned to write a linker script because I wasn't going to use any of that bloated C rubbish. As for the programming software (minichlink), I just opted for now to use a Linux host via ssh for writing to the chip.

Code to follow. ;)

#commodore #c64 #riscv #assembly