💯​ 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!
Yay! Made my way into Imp.v of Software Foundations, where we get to play with a toy imperative programming language.
The first larger exercise was to write an optimizer/simplifier for boolean/arithmetic expressions and to prove its soundness. I managed to neatly separate the actual optimization steps from structural recursion and used (as instructed) a lot of try/repeat tacticals to make the repetitive proofs about as short as their natural-language equivalents.
This was very satisfying. :3
Proving binge continues. My regex matching function that has never been called is correct!
This finishes chapter "IndProp" (Inductive Propositions) of #softwarefoundations and that means I am now fully caught up in terms of chapters with where I left it all those years ago - major milestone!
IndProp is also by far the heftiest chapter in Volume 1, so... not far now.
@ramin_hal9001 @theruran @vollmerm
a friend of mine and I actually started reading #SoftwareFoundations together and it looks amazing; I got Proof General setup and it's super fun. I love using theorem provers, and had started Wadler's Programming Language Foundations in Agda a couple years ago over winter break, but each time stuff came up that made the study time necessary unfeasible.
I have Byrd's dissertation and have browsed it, and think I will probably make it my next deep dive. miniKanren is overall probably the idea in CS that has impressed me the most (I'm a sucker for things with little barrier of entry to understanding the implementation).
I got addicted to category theory around 2016 after finishing a masters thesis focused mostly on ZFC & Cohen's forcing proof in Badiou's Being & Event, and was doing a dissertation on the use of topoi in his value theory, but that effectively came to an end when I discovered and got addicted to Scheme at the beginning of covid.
pesco
\LuXaS
Csepp 🌢
Lucas
blake shaw 🇵🇸
read-only account (Rain 🚱)