Last year I rolled up the newsletter into an ebook and gave my thoughts on every published blogpost. I haven’t gotten around to making the 2021 Computer Things volume, so we’ll just run through the blog posts this time.
I wrote about 39,000 words for the blog, which is about 8,000 less than last year. But I also released a 20 minute video, and was horrifically depressed for half the year, so I’m not too broken-up over it. Here are my thoughts on every blog post:
Hoo boy, lots of thoughts. This was a set of three essays, based on two years of interviewing crossover engineers:
It is the most important work I’ve done since Practical TLA+, and arguably the most important work I’ve done, ever. I was disappointed with how little of a splash it made at the time. Many of my expectations were, admittedly, fantastical. I thought it could spark a resurgent interest in interviewing and interdisciplinary research, doing what I did with other disciplines. I forgot that these things are hard and most people are busy!
That said, there’s also the long tail. I still occasionally get emails from people who appreciate the essays or link them in internet discussions.
On a personal level, the Crossover Project was also a way of proving to myself that I wasn’t just a one-trick pony. I initially built my audience on formal methods, and while that stuff is still deeply important to me, I don’t want to just be “the formal methods guy”. And that means showing I can do good work without relying on a connection to formal methods. I’ve done minor stuff in that regard — empirical engineering, software history— before, but this was my first non-FM Big Project.
I have no idea what my next non-FM Big Project will be. But now I got a lot more skills, so it probably won’t take me two years to do.
Inspired by Ben Kuhn’s In Defense of Blub Studies, I did three posts this year on advanced TLA+ techniques, which coincidentally were in ascending order of complexity. Action properties aren’t needed to use TLA+ well, but they were the first thing that felt cool to me. The first time I used action properties, I felt like I was doing a particularly complex juggling trick, where pulling it off meant I had mastered the essence of juggling.
Helps that action properties are an incredibly useful technique. You use them to verify properties of how a system changes, like “if the kill switch is on, we can’t add new messages to the pool.” You feel cool using them and it meaningfully helps your modeling. This is def something I need to add to learntla when I resume work on it next year.
Back in 2018 I did a tweetstorm:
You’ve probably seen a bunch of rants on why “do thing with linked list” is a terrible interview question. I’d like to explain why “do thing with linked list” is an interview question in the first place. Buckle up everyone, it’s time for some g̶a̶m̶e̶ ̶t̶h̶e̶o̶r̶y̶ HISTORY!
— Hillel (@hillelogram) February 10, 2018
It went viral, motivating me to use it as a motivating example in my 2019 talk on software history. The talk went into considerably more detail about the question, drawing on interviews with programmers from the 70’s and 80’s and lots of analysis of job postings and Usenet discussions. I think the audiences like it, but nobody afterward watched the recording, so I wanted to make the new research publicly accessible.
So, the blogpost. In addition to covering the new evidence, I added a bit on what the process looked like. Dead ends, research techniques, unexplored avenues, etc. The post was popular and people liked it a lot, but mostly in the linked list content, not the skills part. If I really wanted to write a post that taught historiographical skills I’d have to make the primary focus of the talk.
This post also underscored an important law of internet forums: nobody reads the article before commenting. Almost all of the replies on aggregators were people giving their own pet explanations, many of which were explicitly refuted in the article. People saw the title and rushed to answer it.
This was inspired by an experimental tweetstorm (tweetversation?) by Lars Hupel and me:
So @larsr_h and I want to try something new: a COLLABORATIVE tweetstorm. The topic? Why it’s so hard to reuse formally verified code. He’s an expert in verifying code with Isabelle, I use TLA+. Together, we can attack the question from different angles. Take it away, Lars!
— Hillel (@hillelogram) March 15, 2021
We primarily discussed composition in terms of verifying code, so I wanted to write an in-depth article on why specifications don’t compose. And, in the process, teach a bit of linear temporal logic. Because I hadn’t learned my lesson from the last post about “don’t try to do two things in an essay at once.”
Probably the one I’m least happy about this year. I intended it as a pedagogical essay to give intuition, not as an airtight argument. But I presented it as an airtight argument. So lots of people responded with things like “this is only a problem in LTL”, or “Iris solves this already”, etc. Then I lost my temper and mocked a sincere person on Hacker News. Unhappy with myself for doing that.
I still think there’s interesting content here, but it needed to be presented in a way that made it clear it’s an introductory pedagogical overview of why composition is hard. At the very least, the framing should have been “composing specifications is hard”, not “specifications don’t compose”.
Tried to do two things here:
I think I succeeded. Overall a pretty solid article.
I sat on this for a while because I couldn’t think of a good conclusion. I opted for listing some questions I had that I didn’t have firm thoughts on. I like that as a general ending, since it makes it clear that this isn’t a closed topic. There’s more to think about!
(I also feel like this article was padded a Discussion at the end, showcasing that there’s more to think. Had to pad it out.
Uuuuuuuuuugh, changed my mind this was the one I was least happy about. Absolutely phoned-in, because I was referencing it a lot wanted it outside the newsletter. This could have been a good article if I’d put any effort into making it blog-quality. I could have at least found an realistic motivating problem!
I was gonna do a talk on esolangs for Felienne Hermans‘ class, but I didn’t want to lecture at 3 AM my time, so I figured I’d record it all ahead of time. Then I thought hey, if I’m doing this ahead of time, why not try making it a video from the start? I’d record myself in Audacity, learn how to use Resolve, and splice together all the samples and clips into one video. How hard could it be?
Holy.
Shit.
This took somewhere upward of 40+ hours to finish. It was supposed to be 40 minutes and was barely half that. I am glad I did it, and I never want to do it again.
Then, six months later, the video was blessed by the Youtube Algorithm and now has almost 300,000 views. This makes it far-and-away the most popular thing I’ve ever made. Maybe I’ll drop writing and become a Youtuber!
(absolutely not)
Not really a content piece, but late June-ish I read Alien Dreams and fell down the generative art rabbit hole. My thought process:
Hey guyz I’m never gonna be a cool artist :(
(Hillel’s Hosting Tip: Bring out the Art Machine at parties and have people throw in suggestions. You get some crazy shit that way.)
Blub studies #2! A lot of TLA+ experts say refinement is the crown jewel of TLA+, but there weren’t any learning resources for it. And enough people in my workshops asked about it, so I wrote an intro. The post doesn’t cover how to do it well, just what it looks like and why it works. I also included a bit on why refinement often isn’t used, so that people don’t feel like they’re using TLA+ wrong if they don’t use it.
This took me over a year to write. The prose was easy, the hard part was finding a good example. The canonical refinement example is a binary clock to a regular clock. That doesn’t make the ideas or value of refinement evident. Some of the ideas I wrote up and rejected:
All of those were either too uninteresting or too complex for an introduction. Finding good examples is HARD.
(I should really give the canonical example newsletter the full blog treatment.)
The most experimental post of this year. I love exploring unusual writing formats and clickfarm is a very unusual format. And it’s a very challenging constraint! It’s not evident to a casual reader, but the post is technically very intricate, as in it demanded a lot from my writing technique. To give one example, the “wrongness” of the “solution” needed to start slow and gradually escalate. The first weird thing should be easily dismissable as low quality clickfarm, the second weird thing looked like programmer incompetence, and it’s only around the CNF chain that things should be eeriely Wrong.
Also, the setup couldn’t show any competence before the punchline, including web design competence. So no footnotes explaining things, no technically-sound justification for CNF, etc. After that, the punchline needed to hit as hard as possible to shock the reader into both 1) realizing the badness of the prior writing was intentional and 2) knowing that the following writing was going to be genuine. Then there’s the matter of how much text can follow the punchline…
Look, what I’m saying is that this post was a lot harder to write than it looks. I’m super proud of it, despite not many people reading it. If you came into it blind, I hope it surprised and delighted you!
The Alloy 6 release blindsided me. I knew it was coming out and vaguely planned to look into it for a late winter writeup, but then I tried it and was blown away. I wanted to get a post out immediately. Overall it was less than a month between downloading the update and publishing the post. It’s not the greatest writing I’ve ever done, but it isn’t too bad, either. I’m especially happy I was able to come up with a suitably meaningful example on such short notice. Later next year I’m gonna try writing a more involved case study that acts as a general advertisement for Alloy.
This was also the first post where I included custom vector graphics! I think graphics are really useful for explaining concepts. Historically I’ve used TikZ, but I’ll do anything to minimize the amount of TikZ I’m forced to write. So I taught myself the basics of Inkscape and drew some diagrams in that. Took a while to make the first couple of images, but it’s a big improvement over writing more damn TikZ and I think it’ll positively improve the stuff I write next.
Blub studies #3! And the most advanced, introducing a technique I haven’t seen in the wild. As far as I can tell, I might be the first person to think of it! That’s one of the more obscure benefits of being an independent consultant: I can spend a few days exploring a novel technique without feeling like I’m wasting valuable work time. The kind of thing where it doesn’t make sense for an employee to spend a couple days figuring out from first principles, but it does make sense to spend a couple of hours learning from someone else.
Looking back, this year was pretty technique-heavy. I think that’s because a lot of my speculative writing has gradually migrated to the newsletter. Next year I want to reverse that a little and put more philosophical stuff on the blog. I’ve got drafts on interdisciplinary learning, question binders, stuff like that. Other big projects for 2022:
Happy new year! May 2022 suck less than 2021.