Status Updates From Software Foundations, Volum...

turns out imperative programming was just pure functional programming from state to state all along!

just trucked through 2 much easier and much shorter chapters.

one of my secrets to getting thru InductivePropositions chapter was pivoting myself to spending very little time on exercises marked "optional", focusing only on the ones marked "standard".

also, there are at least 2 chapters of volume 1 i'll be skipping, (the class at Penn skips 6)

painfully slow. as it gets harder i get noticeably sadder without the stream of dopamine from completed exercises. my skipped exercise rate is getting atrocious, but i'm not willing to just stop moving forward. I think this is just going to be a preliminary pass that refuses to spend more than an hour on a single exercise (even tho i've invested more than 3 into several exercises already)

almost done some of the harder exercises of ch 5: Tactics

Working on proofs with Coq is so much fun that it's totally destroying my will to go back and do pencil-and-paper proofs on the Lawvere & Schanuel book … but aside from that inconvenience, this is a wonderful hands-on education in proof technique and types.