December 27, 2021

2nd Annual End-of-Year Essay Retrospective

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:

The Crossover Project

Hoo boy, lots of thoughts. This was a set of three essays, based on two years of interviewing crossover engineers:

• Are We Really Engineers?
• We Are Not Special
• What engineering can teach (and learn from) us

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.

TLA+ Action Properties

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.

Why Do Interviewers Ask Linked List Questions?

Back in 2018 I did a tweetstorm:

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.

Why Specifications Don't Compose

This was inspired by an experimental tweetstorm (tweetversation?) by Lars Hupel and me:

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".

Clever vs Insightful Code

Tried to do two things here:

1. Articulate a sense of "cleverness" that exists in my head but I find hard to describe. We use words like "cleverness" ostensively— as a collection of examples, not a formal definition. That makes it easy to think of extreme examples, but not variations of cleverness.
2. Discuss the consequences of this particular kind of "cleverness" vs the conventional sense, aka why it's valuable to see the variations in cleverness.

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.

Cross-Branch Testing

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!

A Brief Introduction to Esoteric Languages

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)

The Art Machine

Not really a content piece, but late June-ish I read Alien Dreams and fell down the generative art rabbit hole. My thought process:

• Wow, GAN art is so cool!
• I wanna be a cool artist, too!
• Oh wait I have no art skills
• Well maybe the GAN artists will think I'm cool if I push the technical boundaries of AI art
• Oh wait I have no ML skills
• Huh, these art generators are really hard to use if you're not a programmer. Maybe if I make a generator that's really easy to use, a lot of people will join the GAN art community and think I'm cool for being the roadbuilder
• Releases Art Machine, DDOSes Google Colab
• Okay bored now onto the next shiny thing

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.)

Specification Refinement

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:

• A hot/cold thermometer, refined to actual temperature values
• Account deposit/withdraw, refined to an event log
• Unordered message pool, refined to ordered
• Reader-writer queue, refined to where the readers have internal state

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.)

How to Solve the Sudoku Puzzle with programming

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!

Alloy 6: it's about Time

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.

Using Abstract Data Types in TLA+

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:

• Update the alloydocs and write a new tutorial
• Restart work on learntla
• Maybe do that damn predicate logic book I started working on last July
• Probably start that "consulting sabbatical" I mentioned before, I'm overdue
• Get back to researching and showcasing cool fringetech, I kinda dropped the ball on that this year

Happy new year! May 2022 suck less than 2021.

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.