February 25, 2021

New Post, Blub Studies, and Theorycrafting

Hello everyone!

First of all, new post: TLA+ Action Properties. It's about specification properties on changes to the state, not just properties on the states. For example, we can use action properties to express "this log is append-only" or "we can only transition from states A → B when x is true." It's a really powerful modeling technique that makes TLA+ a lot more expressive. Check it out!

The piece was inspired by In defense of blub studies, by Ben Kuhn. I'd heartily recommend reading it.

Blub studies is the study of what goes on in the guts of these boring, everyday systems—not the kind you get tenure for inventing, but the kind people actually use.

Blub studies is a never-ending treadmill of engineering know-how. It’s the fiddly technical details of how Git stores data, or how Postgres locking semantics caused your migration to bring down prod, or why pip install failed this time.

His thesis is that most people get far more use out of studying blub than studying new frontiers or deep fundamentals. The essay sort of wavers a bit on whether blub includes all practical knowledge (as in his React example) or just the implementation details of technologies, but I think he mostly means implementation details, while I think I'm using it more broadly. A lot of my TLA+ expertise is blub:

• Knowing the syntax for everything, like [][P(x)]_x for action properties or how to write a set reducer.
• Knowing the weird pitfalls, like the cases where P /\ Q => R is parsed as P /\ (Q => R).
• Being able to read the error messages while also knowing the cases where PlusCal translation fails without producing an error message.
• Knowing how to optimize a model or test if it's unbound.
• Knowing what valid TLA+ expressions cannot be checked by TLC.
• Knowing where to find the documentation on tlc2.TLC command-line flags.

All stuff that isn't "core" to TLA+ but is really valuable for using it at scale. Stuff that can take a beginner hours to figure out that I can diagnose in a second. Blub studies.

Blub studies provide a critical bridge between beginner and advanced users of something. I don't think it's possible to become an expert in something if you don't also know its blub. And like any other topic, blub is easier to learn than to discover on your own. So if I want to make FM more popular, I need to provide more information on FM blub. I have a few more pieces drafted out.

Theorycrafting

Another type of writing I've been thinking a lot about: "Theorycrafting". This is informative content caveated with "not based on experience". You just thought really hard about something, came up with ideas, and wrote them down. One example would be Decision Table Patterns. A lot of the techniques there aren't things I've used in practice. I was just writing down techniques I thought could help in these cases. Pure theory.

I've always been a bit torn about theorycrafting. There's an obvious problem that I don't actually know if it works or not. Lots of things sound good in theory but fail in practice. Not only do I not know if it works, I have no information on whether it works. It's just an idea I had. Is that worth sharing with people?

I guess it's okay if I make it very, very clear it's theorycrafting. Then people can read it and go "oh, this is purely an idea, he's not advising it, just proposing it." In return, I get a chance to talk about ideas, because ideas are interesting. There's a lot more ideas I want to share than I can reasonably flesh out and test in practice. At least the idea gets to be out there. If other people find it interesting, they can explore it themselves.

(One of the highest compliments I've ever received was when Cross-Branch Testing inspired Phillip Schanely to add diffbehavior to Crosshair. He saw an idea I had and liked it enough to make it real.)

The other downside of theorycrafting is that it might be too "low-content" for people. I know a lot of devs follow me for my expertise in formal methods, not for my ideas. But I think that if I put just as much love and care into my theorycrafting writing as I do into my essays and blub studies, people will be okay with that.

So yeah. More blub studies, more theorycrafting this year. Also probably more journalism. I've already forgotten how much interviewing for the Crossover Project sucked and am planning out the next project. It will be very silly.

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.