Finally done with conferences and glad to be back in Chicago. Next big event is the TLA+ workshop on October 16, which still has slots available! The faster I can fill those up, the sooner I can stop putting advertisements in my newsletters. I don't like doing it any more than you like reading it. Use the code C0MPUT3RTHINGS for 15% off.

Keeping on the topic of TLA+, I saw this question on linkedin:

I've always wondered - is there much use of building formally verified software on top of non-formally verified systems (like the OS the software runs on)? To me, the absolute layman here, it feels like we're building proofs on top of potentially/probably flawed axioms. If we can verify Raft is a solid algorithm but it's built on non-verified networking devices do we end up putting a wrong amount of trust into the system?

This is the impossible problem of trusting trust: is formally verified code really provably-correct if it's compiled with an unverified compiler? What if the code's correct and it's running on an unverified OS? You could use a verified OS like seL4 but what about the hardware itself? What if the hardware design is proven but the manufacturing process adds a backdoor? Verifying the whole process is too hard for anybody but the richest countries. So why do formal verification at all?

Extra late because I just got back from Australia and slept 16 hours

Thanks to everyone who reached out last week! I'm still wrapped up with travel and Strange Loop but should start getting to them next week. Also, I'm teaching a TLA+ workshop on October 16! Register here, use the code C0MPUT3RTHINGS for 15% off.

There's this quote I like, "the best model checker is your brain." People who do formal methods find that simply writing the spec is enough to find errors, even without actually running it. It's kind of like if writing a unit test on a piece of paper told you where the bug in your code was.

I was in Australia to attend YOW! Perth, and one of the closing keynotes gave me a good way of describing it. Katrina Owen gave a talk on how to quickly build "expert intuition": perceptual learning. Take a large category of situations and classify them. The canonical example would be chicken sexing. Imagine you're given a day-old chick and asked to guess the sex, then told if you're right or not. If you do this thousands of times, you'll eventually be able to consistently get it right, even if you aren't actively studying specific rules.

The October TLA+ workshop still has some slots left! Register here, use the code C0MPUT3RTHINGS for 15% off.

I wanted to write some stuff on TLA+ modeling here but was at a conference and vastly overestimated the amount of writing I could get done. I presented the "Are We Really Engineers" talk and got a really positive reception, which I'm super happy about! And that means it's time to finally consider the Crossover Project complete and move on to my next planned project.¹ Working title:

The Case of the Missing Data Type

A directed graph consists of node elements and edges between nodes. Nodes and edges can optionally include data attributes. Some business domains representable as directed graphs include transit routes, org charts, food webs, and webpage links. Some computer domains representable as directed graphs include package dependencies, state machines and DFAs, state spaces, garbage collection, Markov processes, function calls, control flow, workflows, ETL jobs, foreign key relations, neural networks, and hash tables (yes, really).

Greetings from Australia!¹ It's the morning of September 5th for me and the night of September 4th in the US. In two weeks when I fly back, I will leave Sydney at 9 AM and arrive in Los Angeles at 6 AM, that same day.

Timezones are annoying enough for regular people, but us software engineers have to deal with the fallout. Then you add in the political aspects and, well, you can't always store all data in UTC.

So what makes time zones so bad?

Look a distraction

First of all, new TLA+ workshop! October 16th, details here. Use the discount code C0MPUT3RTHINGS for $100 off.

But enough about business, I'm here to complain.

My painful, fruitless quest for programmable slideshow animations

I'm giving the Are We Engineers talk in Perth September and looking over the slides has reminded me of how much I hate slides. I started with PowerPoint but switched to Beamer in 2018 or so, which is a LaTeX package for making slide decks. Unlike PowerPoint, it's a text file, which is makes version control and synchronization a lot easier. But then I saw some really good slide decks and realized that if I wanted to give the best talk possible, I'd have to make really good slides. I don't have an eye for design and I tweak my talks too regularly to pay a designer to "bake" them.

New blog post, which is also a new project: Learn AutoHotKey by stealing my scripts. It's about this project. Patreon notes here.

This is my second "educational codebase", after TLA+ Graph Modeling. The idea's been stuck in my head for a while. A common bit of advice to new coders is "get better at programming by reading code." The problem is that codebases aren't set up to be read. While we prize readability in our code, that's readability for other contributors. There's certain things we can assume for other contributors that we can't assume for beginners. Take the most starred codebase on GitHub, react. Here's a chunk of one file:

// $FlowFixMe[missing-this-annot]
function Chunk(status: any, value: any, reason: any, response: Response) {
  this.status = status;
  this.value = value;
  this.reason = reason;
  this._response = response;
}
// We subclass Promise.prototype so that we get other methods like .catch
Chunk.prototype = (Object.create(Promise.prototype): any);
// TODO: This doesn't return a new Promise chain unlike the real .then
Chunk.prototype.then = function <T>(
  this: SomeChunk<T>,
  resolve: (value: T) => mixed,
  reject: (reason: mixed) => mixed,
) {
  const chunk: SomeChunk<T> = this;
  // If we have resolved content, we try to initialize it first which
  // might put us back into one of the other states.
  switch (chunk.status) {
    case RESOLVED_MODEL:
      initializeModelChunk(chunk);
      break;

Now think about all of the JavaScript features and concepts this uses: prototypes, promises, switch statements, underscore fields. It's also got a lot of flow features, like annotations and generics, which aren't clearly distinguished from the JavaScript concepts! A beginner reading this would be hopelessly lost. Maybe there's a better React file to start with, but how is our beginner supposed to find it?

The halting problem is "undecidable": there's no algorithm which can tell you if an arbitrary program with an arbitrary input will halt or not. IE, if you give me a proposed "halt-detector", I can inspect it and come up with a program and input for which it would give the wrong answer.

Most people think that's a cool mathematical theory but don't know the real world relevance, because computers aren't Turing machines and have finite memory, so all programs are guaranteed to halt. I once saw a keynote speaker say their programming language was stronger than Turing-complete because all programs in it had a timeout, and so they solved the halting problem.

To better understand why the halting problem is so important, it's better to look at what the world would be like if it was solvable.

If you take a square and rotate it 90 degrees, you get back an identical square. We say the square is rotationally symmetric. Similarly, if you reflect it across an axis, you also get the same square. Since "reflectionally" isn't a word, we can more generally say it's "symmetric under reflection".

If you take any two numbers and compute x + y, you'll get the same answer if you instead compute y + x. We say that addition is commutative, but it's just as correct to say it's symmetric under transposition of terms. Subtraction is symmetric under "double-increment" (x - y = (x + 1) - (y + 1)) while multiplication is symmetric under skewing (x*y = 2x * y/2).

In formal specification, we can express symmetries as properties of the system. Most commonly this is transpositional symmetry. If F(x, y) is some predicate (boolean function), then F is symmetric if

all x, y | F(x, y) => F(y, x)

I just added a big new section to learntla: Optimizing TLA+ Model Checking. I take a spec and then show 15 different optimizations, many of them getting a 10x runtime improvement. Patreon notes here. Besides that I've done very little writing the last couple weeks. I'm just in a slump: I sit down to write and the words all come out wrong. It happens sometimes and there's nothing to do about it but wait it out.

So instead of working I've been learning Raku.¹ It originally got on my radar after I ranted about dynamic languages and a couple of users told me I'd like Raku. I finally checked it out last week to see if it'd make a good "calculator language". I use a hodgepodge of Python, J, Frink, and Excel to do math and they all have their own big drawbacks, so it'd be nice if Raku could round them out.

After several days of experiments, I'm at a loss of how to describe Raku. The best I can come up with is that the language was designed by a bunch of really intelligent gremlins. Gremlins who spent a lot of time gathering feedback from other gremlins.

Weird Operators

1. If you're on a repo main page and press . then you open it up in "github.dev": an online VSCode instance where you can make edits to code, push commits, and review pull requests inline.

   

2. If you click on your profile picture in the upper right corner of the screen, you get an option for "feature preview", which lets you add experimental features to your github. For example, you can enable rich Jupyter diffs and make ctrl+alt+k open a command palette.

3. You can regex search code, both in a repo and sitewide, by wrapping the search in /slashes/. /^hash.?map/ matches "hashmap", "hash_map", and "hash map", but only as the first word of a line. You can also search ranges in metadata, like projects with at least 20 stars.
4. Press Y in a repo to change the URL from branch-based to canonical commit-based. Press I in a PR to hide comments. Press A to hide the "build failed" annotations (h/t Martin Janiczek).
5. I mentioned github.dev, right? Did I mention that you can use it on other people's repos, it'll save your work across browser sessions, and it'll only fork the repo if you try to commit?

6. If you're commenting on a PR and put a backtick-codeblock labelled suggestion in the comment, it'll show it as a line change:

   

7. There's an online graphql IDE so you can do graphql queries without having to set anything up locally. I haven't used it yet but I think it'll be a really handy research tool!

I'd call these all "undocumented" features except they are documented, in the official documentation, it's just that nobody reads documentation anymore. GitHub's been trying to integrate some of these features into the UI but nobody presses random buttons on UIs either. I've not been able to find any "GitHub tips and tricks" resources; if there is one, it's camouflaged by all the pages for git tips.¹

So instead I'm getting the word out with an email blast. Seriously try the . thing it's super duper useful

I'm going to a small academic workshop on design next week. This got me thinking of the various meanings of "design", which got me thinking about the various purposes of "design", which got me thinking about queryability.

A system is queryable if (and I'm speaking very roughly) you can easily retrieve information you need from the system data. As an example, let's say we record scientists and the papers they worked on. You could represent the data like this:

Scientist {
    name: str
    department: Department
    papers: set of Paper
}

Paper {
    name: str
    published: date
}

In this model, it's easy to query the papers a scientist worked on, it's just one lookup. On the other hand, it's really hard to get all of the authors of a given paper, we'd have to iterate through all the Scientists to find out. Alternatively, we could do this:

I was gonna write an rant about the potential probabilistic model checking, then realized I needed to look at projects besides PRISM and STORM. Then I checked out simpy and saw it had a Defense of Design (DoD):

This document explains why SimPy is designed the way it is and how its design evolved over time.

This is great! More projects need this!

All languages and projects do "odd" things that make no sense to outsiders. And oftentimes there's a good reason, like

Recently the piece Integrated tests are a scam was making the rounds. I was going to write a rebuttal, but it comes prerebutted by the author himself, who says in other places that integrated tests are not integration tests, that integrated tests are good for non-basic correctness, and that the problem is actually integrated tests without unit tests. I wonder if this original article was a response to testing trends of late 00's, which 10 years later now reads like an overcorrection.¹

I could look into that, or I could take one of his points and freebase a completely different topic. Here's two critical steps in his integrated test death spiral:

1. We write more integrated tests, which are bigger and don’t criticize our design as harshly as microtests do.
2. Our tests don’t give us as quick nor strong feedback about our design as they could, and we’re humans, so we design things less carefully than we could. We design more sloppily both because we can get away with it and because we don’t notice as easily that it’s happening.

So the problem is that integrated tests are bigger, take longer to run, and "don't give as quick or strong" feedback as unit tests. Or, more fundamentally, unit tests are a fast feedback loop while integration tests are a slow feedback loop.

Sorry this one's late! Between the holiday, working on a bunch of longform pieces, and AI War 2 I've been behind on writing. First up, new blogpost! It's about the "four document model" that Divio and many others use for writing about their tools and my problems with it, specifically its limitations. Still a good model, just has drawbacks.

I've also been doing a few upkeep things. One is going through and replacing all the Twitter embeds on my website with images. Another is to going through all my Twitter dump to see if there's any ideas I should rescue for the blog or newsletter. There's some stuff I really liked there and I don't want it to die with the hellsite.

One of my favorite tweetstorms was about the intersection of my work and my biggest hobby. As some of you may know, I'm an avid chocolatier. I got into it in college but only really picked it up in 2015. If you run into me at a US conferences odds are I'll have some to hand out.

Harold Abelson once said that code should be written for humans to read and only incidentally for computers to write. It follows that, like any form of communication, code can carry emotions. Programming perversity, then, is code that conveys morbid fascination, the kind of amused horror where you cover your eyes but peek through your fingers. Take some innocuous features of a programming language and then bend it all into a pretzel. Congratulations, you've made performance art.

The IOCCC, International Obfuscated C Code Contest, was the first mainstream programming perversity. This is the winner of the 1985 contest:

#define P(X)j=write(1,X,1)
#define C 39
int M[5000]={2},*u=M,N[5000],R=22,a[4],l[]={0,-1,C-1,-1},m[]={1,-C,-1,C},*b=N,
*d=N,c,e,f,g,i,j,k,s;main(){for(M[i=C*R-1]=24;f|d>=b;){c=M[g=i];i=e;for(s=f=0;
s<4;s++)if((k=m[s]+g)>=0&&k<C*R&&l[s]!=k%C&&(!M[k]||!j&&c>=16!=M[k]>=16))a[f++
]=s;if(f){f=M[e=m[s=a[rand()/(1+2147483647/f)]]+g];j=j<f?f:j;f+=c&-16*!j;M[g]=
c|1<<s;M[*d++=e]=f|1<<(s+2)%4;}else e=d>b++?b[-1]:e;}P(" ");for(s=C;--s;P("_")
)P(" ");for(;P("\n"),R--;P("|"))for(e=C;e--;P("_ "+(*u++/8)%2))P("| "+(*u/4)%2
);}

It prints a random maze.

Alloy is a formal specification language I use a lot. In Alloy, ≈all data is either an atom or a relation between atoms.

sig DataSource {}

sig Step {
  requires: set Step
}

Unlike most languages, Alloy has two notions of subtyping: a type (or "signature") can be extended, which is exclusive, or they can be in, which are stackable. In this example, the source can be generic, a database, or a file, but not all three. The Step can be generic, an extraction step, a load step, or both:¹

sig Database, File extends DataSource {}
sig Extract in Step {
  from: DataSource
}

sig Load in Step {
  to: DataSource
}

You may have heard of this new idea called "Agile", where you prioritize people over processes etc etc etc. I occasionally saw it on Twitter, before I quit that hellsite, after which I kinda lost track of it. But I recently started clout-mining LinkedIn and now see see a lot more posts about Agile. I think it's almost mainstream!

Like any idea that picks up steam, people are now disagreeing on how to actually do Agile. There's Scrum, and Kanban, and SAFe, plus techniques like mob programming and planning poker. Other people argue that all this praxis is missing the point of Agile. As one person puts it:¹

The Agile Mainfesto is 73 words. Gobs and gobs of software has been written to "do agile". Every software shop I've encountered in the last decade has told me they use an agile software development process. Being an "Agile coach" is an entire career. But the whole manifesto is just not all that. The entire body reads as follows:

We are uncovering better ways of developing software by doing it and helping others do it. Through this work we have come to value:

1. Individuals and interactions over processes and tools
2. Working software over comprehensive documentation
3. Customer collaboration over contract negotiation
4. Responding to change over following a plan

That is, while there is value in the items on the right, we value the items on the left more.

That's it. Focus on relationships with people, and actually solving problems.

I see this sentiment all over the net: everybody is making Agile too complicated; just follow the principles and do your best.

Hello everyone!

Monday was the final TLA+ workshop of the season! I'm finally done with workshops and all outstanding consulting gigs, leaving the whole summer free for writing and projects. And like, learn new tech in general. Maybe I'll pick up Rust again. Who knows.

I haven't been thinking too much of new ideas, but one came up last night about how everyday programmers can use a concept from formal methods. In FM we have a notion of property strength, defined as

STRONG => WEAK

I finally updated the alloydocs to Alloy 6. The docs now cover how to use temporal operators in Alloy.

To celebrate, let's talk something completely unrelated. The simplest kind of collection is the set: an unordered collection of unique elements. All branches of mathematics use sets somewhere, and in fact you can bootstrap all other collection types from just sets. Many programming languages have set types or something that mimics sets, but it's less common than sequences, which are ordered collections of repeatable elements. ≈All programming languages have some form of sequence.

If sequences are sets + two properties, what are sets + one property?

I normally don't do either hot-off-the-press writing or "tech news" opinions, but the Vision Pro announcement touches something near to my heart and I want to talk about it. No plan here, just writing and seeing where it goes.

I've mentioned before that I don't have a CS degree: in college I did math and physics. When I was 11, I read in _The Physics of Star Trek) that Caltech scientists successfully did teleportation in a lab. As soon as I saw that I stopped wanting to be a game designer and started wanting to be a physicist. There's something ineffably wild about what I'd read, outside the bounds of mundane society, thrilling and terrifying in equal measures. I had to be part of this!

Turns out that The Physics of Star Trek misrepresented the research,¹ actual physics looks nothing like a preteen's imagination, and grad school is scary. So after getting my undergrad degree I moved to SF to get a job as a programmer, because I really liked computers and it paid well. And that was… fine, I guess? I spent two years as a Javascript grunt in a Rails shop which is a pretty good way to burn out anybody's love of programming. I think at one point I threw away my personal computer, that's how little interest in programming I had. There's no wilderness in software.[^software]

And then comes the goddamn Hololens demo!

GOTO Chicago is over! My talk, "Is software engineering really engineering", went over pretty well, and I'm happy with how it turned out. I'm going to try submitting it to other conferences. Beyond that, I have a TLA+ workshop I'm teaching on June 12th and after that my next engagement is in September, so there's a lot of time to take up with things.

(Use the code C0MPUT3RTHINGS for 10% off the TLA+ workshop! It's a full day of hands-on experience, plus I give my students followup reviews on their specifications.)

In the talk Q&A, one person disagreed with me with something I thought was really interesting and deserved a longer response.

My original claim

This is a really busy week for me, so light newsletter this time. Let's start with obligatory stuff and then get into fun newsletter stuff.

Announcements

So first off, I just finished the May TLA+ workshop. This is the first time I felt really happy with the material and that I won't have to do a week of revisions before running it again. Speaking of which, the last workshop (for now) is June 12. Due to a couple of surprise expenses I'm trying to get a bigger attendance for this one, so I'm dropping the price from $749 to $649. Use the code C0MPUT3RTHINGS for an additional 10% off.

Next, I'm speaking at GOTO Chicago next week. My talk, Is Software Engineering Real Engineering, compares and contrasts software from "real" engineering, based on interviews with 17 people who've done both. Turns out that I have a 10% discount coupon, hillel10, which takes the conference from $2395 to "merely" $2155.

People always talk about "P vs NP" like P problems are easy and NP problems are hard. This is a useful day-to-day model but also an oversimplification.

Problems can get way, way harder than NP.

(If you want a brief refresher on P and NP, check out my post NP-Complete isn't (always) Hard.)

PSPACE-complete

Last week Madhadron's 2021 piece The seven programming ur-languages went viral. One I saw a lot was "where does TLA+ and Alloy fit into this?"

Hoo boy.

I've been dreading this one. You see, TLA+ and Alloy don't fit into any of the programming ur-languages, because they aren't programming languages. They are specification languages (SLs) and are designed for modeling systems, not implementing them. While there's a lot of intermixing, SLs come from a different lineage than PLs and we need to treat them separately.

So, someone has to write "the seven specification ur-languages", and I really don't want to be that person for three reasons:

Hi everyone!

First of all, new blog post: Somehow AutoHotKey is kinda good now. AHK's been a core part of my toolkit for years now and the new, backwards incompatible version is a whole lot better. But most of the article is about how much v1 sucked, which is more entertaining and more useful to non-AHKers. You think Javascript is bad? Javascript's nothing compared to v1.

I wanted to write a newsletter that was topical to the post, but none of my ideas really gelled, so instead here's something else on my mind: when is OOP inheritance better than composition? I'll assume you've all heard "prefer composition to inheritance", which is generally good advice, and I'm interested in where the advice doesn't apply.

(Caveat this is mostly theory crafting. I've run into a lot of cases where this approach seems correct but I wouldn't be surprised if someone found a "better way" without using inheritance.)

We're just twelve days from the TLA+ Workshop! Right now the class is just a quarter-full, meaning it's going to be a lot of really focused individual attention. If you want to join in the fun, use the code C0MPUT3RTHINGS for 15% off.

I make most of my money off teaching workshops, and that means I put a lot of time into thinking about how to teach them better. Most of that goes to lesson planning, topic order, pedagogical improvements, etc. But I also regularly write assistive programs. See, there's two sources of complexity in workshops:

• Essential complexity: students not understanding the mind-bending core material.
• Accidental complexity: students getting bogged down on unfamiliar notation and syntax errors, getting distracted and falling behind, forgetting to download the class materials, having a last-second emergency that calls them away for half an hour, etc etc etc. This doesn't necessarily prevent students from learning, but it wastes time and frustrates everyone.

The workshop must to handle the essential complexity. If it doesn't, it's a bad workshop. The workshop should handle accidental complexity. If it doesn't, it's not a great workshop. The problem is that the accidental complexity is much broader and less predictable. You can lesson plan your way through the essential complexity, but not the accidental complexity.

On March 24 I wrote GPT is revolutionary. On March 27 I got access to GPT4.¹ Now that I've used it for a month, I'm firmly in the "this is the greatest thing ever" camp. And, much like my experience at Burning Man, I'm finding a not-insignificant number of my fellow campers run around with their butts showing. GPT4 needs advocates that aren't either SEO marketers or AGI fanatics, so here's why I like it so much!

I first tried it out when writing Everything's an API: I wanted to cite an interesting case I knew about but couldn't find the sources I needed. So, as an experiment, I asked GPT4:

Now I should make clear that the AI got the details wrong. The article was written by Gary Taubes, not Adrian Thompson, and it was published in 1998.² However, it got the name of the article right! I hadn't been able to find the article by searching, and GPT4 just... gave it to me.

No-code/low-code is the new hypename for tools that help you Do Computer Stuff without needing (much) programming skills. There are lots of tools in this space, most targeted at businesses, many selling themselves with "you won't need a software developer". I think the first use of low-code was in 2011 but this kind of "rapid application development" goes at least as far back as Visual Basic 6.¹ Many no-code tools are visual builders, which looks "easier" to nontechnical people.²

Professional programmers, as a rule, do not like no-code. Arguments include:

• No-code apps don't scale beyond a low complexity ceiling, then you're SOL
• You need a lot of technical knowledge to use them properly, which defeats the whole point
• The hard part of SE is figuring out the solution, not coding it up
• All the no-code sites look eerily similar to each other and it really creeps me out.

Hi everyone,

I wrote a new blog post, Breaking the Limits of TLA+ Model Checking. It's the first (non-learntla) TLA+-related content I've put out in what, almost two years? It also comes with a GitHub project with all the software artifacts: the spec, the graphing software, the scripts, etc. It's about how to test the things that TLA+ can't natively check, like hyperproperties and probabilistic properties.

So what do I mean by "things that TLA+ can't check?" I spent ten minutes writing and rewriting two paragraphs carefully defining the differences between the language and the model checker before giving up and saying "this is a newsletter, nobody wants to read this." So here's the oversimplification. In TLA+ we have a spec that has multiple behaviors, or traces. Properties in TLA+ are things that are true for every behavior. Some such properties:

• "Two threads can't both be in the critical section": True if in every behavior, there isn't state where more than one thread is in the cs.
• "The light cannot go straight from green to red": True if in every behavior, there isn't state where the light is green followed by a state where the light is red.
• "The algorithm eventually gets the right answer": True if in every behavior, there is a state where the answer is correct.

When I went on Windows full time in 2019 I decided to avoid WSL as much as I could, which meant learning the Windows-native ways of doing things, which meant learning PowerShell. It was a pretty rough start! There are some affordances for people used to bash, but anything more complicated than "copy a file" doesn't translate at all.

Once I got more used to it, though, I found that I really like powershell. It pushes the boundaries of what can be "shell scripted" and what needs a "proper" programming language. I don't think I'll convince any Mac or Linux folk to switch to powershell core,¹ but I can try convincing Windows people to stop using bash through WSL. And okay, maybe make a few bash users go "damn I want that trick".

The autocomplete is very good

Everybody who's seen Powershell knows how verbose it is. Instead of cat, you write Get-Content. That sucks to type! In practice though you're not typing long strings very often. Part of that is because PS comes with a default cat alias, but it's also because PS has very, very good autocomplete.

TLA+ Workshop + Review

I'm running a TLA+ Workshop in May! Use the code C0MPUT3RTHINGS for 15% off. As part of the purchase, I'll do a spec review of a spec you write after the workshop. As an example, here's a 1-hour review I did of a spec from February cohort. Thanks to Cory Myers for letting me share the review!

The Capability-Tractability Tradeoff

The more things your system can represent, the less you can say about the things that are represented.

Hi everyone!

My April Cools piece is up! It's about really weird stuff you can buy online. Now I know that's standard SEO farm stuff, but I promise I put a lot of time into researching why people actually want to buy these things. If you ever wanted to know where carnivals buy and sell their rollercoasters, now's your chance.

Anyway, that's just the April Cools for the blog. I've also got one just for the newsletter! It's about what to do with spare hotel keycards.

Hi Everybody,

April Cools is this weekend! A bunch of people who normally write tech stuff will be writing about a bunch of other topics. If you've got a blog and find April Fools to be eye-rollingly trite, come join us! You don't need to pour your heart and soul into a 10,000 epic, just write something fun and genuine and out of character for you.

I've got a lot on my plate this week, so I'll keep this newsletter short and sweet. Hyrum's law:

I don't feel comfortable making predictions about the future. There's just too much that goes into it and it's way too easy to be wrong. But if I don't occasionally write my riskiest thoughts, do I really deserve a newsletter?! If this ends up being wrong, I promise I'll do a postmortem. Here goes:

I think GPT-4 will be revolutionary. I think ChatGPT already is revolutionary, and in fact the revolution started in February, when OpenAI released ChatGPT Plus. We haven't seen the full consequences of it yet.

Half of you are thinking that I'm saying the obvious and the other half think I drank the AI koolaid. I think I'm approaching in a very slightly different way than most of the stuff I've read, so please give me a chance to justify why I think this is a big deal.

GPT is different from other AI hype cycles

Hi everyone! It's two days after the March 20 TLA+ workshop, which means it's time to start getting feedback and revising things for the May 15th workshop. At some point I want to talk about my "workshop technology" I use, but that'll take some time to write up, so maybe next week? We'll see.

(If you're on the fence about the workshop: attendees can share specs they write after the class and I give them feedback. So not only are you learning TLA+, you get help applying it to your job!)

Anyway, here's a software engineering idea I've been playing with but haven't tried in practice yet, so I don't know how well it works. Constraint solving¹ has this technique called "channeling constraints", where you represent data in multiple connected ways. Like if you're constraint solving a schedule, you have two possible representations of "which talk is in slot T and room R" (in MiniZinc):

Making memes

I'm ahead of schedule on workshop prep, which means I have time to think about things besides pedagogy and formal methods. And I've been thinking of a kind of article I commonly write:

1. Here's some examples of something.
2. I am going to give that thing a name.
3. Now that we have a name, let's discuss it as its own topic.

Examples: edge case poisoning, mimicry, cleverness vs insight, constructive and predicative data.

We're just one week from the TLA+ workshop! Thanks to everyone who signed up, and if you're interested, there's still two slots left!

I also published a new blog post, A Neovim Task Runner in 30 lines of Lua. It's about a little Neovim script I wrote that can handle tasks like "execute this script on whatever file is in the left window, with whatever flags are in the active buffer's b:flags variable. Yes, this is something that I actually needed. I have weird problems.

For the newsletter, the important bit is the "30 lines" part. There's a lot of reasons why we program, but a major one is automation of manual tasks. For most people, the tradeoff is not between language A and language B but between language A and doing the task by hand.

Now for the obligatory XKCD:

Sent to me via mailbag:

Have you used TLA+ to model resilience as in resilience engineering (systems in general)? — Feodrippe

Resilience Engineering, to my understanding, refers to building systems that can function in the presence of disruptions. For example, if a backend service gets overloaded, its dependencies can automatically switch to fallback logic to keep serving customers and give the service time to recover.

I've not done much work personally with "resilience engineering". But the idea comes up a lot in formal methods, in the form of resilience properties. These are goals of the systems that we want (and use resilience engineering) to achieve. And I think the details of resilience properties are interesting enough for a deep dive. I'll use syntax, but it should be applicable to other specification languages, too.

Two years ago I started a new book: Predicate Logic for Programmers. In it I said

People often ask me what’s the best math to learn for formal methods, and my answer is always “predicate logic”. 1 It’s super useful to specifying properties, understanding requirements, and just modeling things in general. Then they ask me how to learn it and I falter.

I estimated it would be in early-access by June 2021. But then real life intervened, and then ADHD happened, and then I didn't touch it for two years. In January of this year I picked it up again, with the goal of having the first draft done by the end of winter. Well, that's not happening either, but I am 10k words in, so that's progress! Let's do a rundown of what the book is, what I have planned, and what I'm struggling with.

Goals and Themes

I promised an update on the logic book today but I haven't done a spite write in a while and oh boy a new one is just raring to go. Update is queued up to be sent out Monday.

Anyway, the candidate for today is The Great Gaslighting of the JS Age. The author Jared White looks at the current spike in React Discourse and claims that the pro-React arguments are identical to last decade's pro-Angular arguments. This means that pro-React people are gaslighting everyone else.

I’m angry because for the past decade of web development, I and so many others like me feel like we’ve been repeatedly gaslit, and that so many of the “merchants of complexity” refuse to acknowledge the harm that’s been done.

There has been a small but mighty ecosystem of “influencers” peddling a sort of “pop culture developer abstractions” ethos on the web whether it’s about React, or CSS-in-JS, or Tailwind CSS, or “serverless”, or “microservices”, or (fill in the blank really)—and they’re continuing to gaslight and obfuscate the actual debates that matter.

I don't have a dog in this fight. I learned formal methods to avoid writing CSS. I don't give a single shit about React versus Vue versus Vanilla JS. But I do care about honest writing, and I especially care about mental health, and I want to say that calling this gaslighting is complete bullshit.

Hello everyone! It's finally March, or at least close enough to March for my purposes. First thing, we're a month off from April Cools! April cools is a less-cringe version of April fools, where content creators like me publish content that is both genuine and totally out of genre. Last year I took a break from software engineering to write about microscopy. Other people wrote about singing church music, marathon food, and how to read rot13. If you've got a blog, I'd heartily recommend joining! It's a lot of fun.

Anyway, between that and a bunch of work obligations, this is going to be a real busy month for me. I'm still committed to updating the newsletter six times a month, but it might be a bit erratic: instead of the alternating 1-2-1 schedule I've been on, it might be 2-2-0-2 instead. Just a heads up.

(If you want to make the newsletter a little easier on me, why not send in a question? If I get a critical mass of questions, or one really really deep question, I'll do a newsletter about 'em.)

Now, two of the things this month are related: the TLA+ workshop in March and the predicate logic book I'm working on.¹ Predicate logic is a necessary requirement for using TLA+ well, but also has a lot of uses outside that. So I'm always trying to figure out how to teach it better. And two topics in predicate logic cause me the most trouble:

Administrative Stuff

• Just one month until the March TLA+ Workshop! Thanks to everyone who already signed up, I'm in the process of revising everything and am real excited to share the new content. There's still nine slots left if you want to join!
• I have a new blog post up: NP-Complete isn't (always) Hard, about NP-complete problems and modern SAT solvers.

Code review vs code proofreading

So in my last newsletter I had an aside on code review:

For some inane reason, Github classifies me as a "major open source maintainer", which means I get a free copilot subscription.¹ I've been using it for a couple months now and I got to say, it's a goddamn delight. It can write boilerplate like nobody's business. I find the tool works best when I'm using it as a keystroke saving device, where it writes 1-2 lines at a time. I write x = and it completes with really[long][dict][lookup]. It's all very easy.

And this easiness worries me. I got a lot more worried when I read What Do ChatGPT and AI-based Automatic Program Generation Mean for the Future of Software, by Bertrand Meyer. He starts by testing ChatGPT with a tricky spec:

I like to use the example of a function that starts with explicit values: 0 for 0, 1 for 1, 4 for 2, 9 for 3, 16 for 4, 25 for 5. [...] This time I fed the above values to ChatGPT and for good measure added that the result for 6 is 35. Yes, 35, not a typo. Now, lo and behold, ChatGPT still infers the square root [sic] function!

About what I expect. After he told ChatGPT that it was for 6, ChatGPT gave back a giant if-else chain. This technically is compliant with his spec but doesn't capture the spirit of what he wants. A good example of the limits of the tool.

It's well-established consensus that software is slower and more bloated than it was 20, 40 years ago. One explanation is that software engineers don't care about their work. Another is that it's the interplay of a lot of different factors and blaming it on apathetic devs is a convenient way to avoid understanding the actual problems.

This post isn't about that.

This post is about the other side of the coin, blaming it on apathetic consumers:

If you poll your existing customers about what you should work on next, they’re going to ask for features, not speed—unless the software is so slow it borders on unusable. And god forbid any red-blooded board of directors would allow the company to take a six-month detour from its product roadmap to work on technical debt. The pressure is always on us to build features, features, features.

Programmers want to write fast apps. But the market doesn’t care.

Programmers want to write bug-free apps. But the market doesn’t care.

I spent the past few weeks thinking about complexity and poking dead birds and stuff, but now that the March TLA+ workshop is available (use C0MPUT3RTHINGS for 15% off!), I'm back in teacher mode and making workshop improvements.¹ TLA+ is intended for finding flaws in software designs. But what else can we do with it?

Creative Misuse is the use of a tool in an unintended way. For example, if you use a screwdriver to pry something open, or a book as a monitor stand. Creative misuse in software includes making games in Excel spreadsheets and using yes to test for broken hardware. Creative misuse is 1) very fun, and 2) expands the space of how useful the tool is. I love finding creative misuses for tools. Here's a few of them for TLA+.

Data Generation

In most programming languages, we construct values step-by-step. In most formal specification languages, we instead take a big set of all possible values and then winnow them down with predicates. This is less efficient, which is why programming languages don't do it, but it's also a lot more expressive.

I recently had to help a friend debug a Word issue where fonts would randomly change to Greek symbols. It got me thinking about theories of debugging in general. At my last job, I was the Debugging Guy. I'd semiregularly have a sprint task like "this other team is seeing a weird behavior in an old system, help them figure out what's going on." I was pretty good at it, but I couldn't explain what good debugging looked like to other people.

Since then, I found a couple of good resources. First is Julia Evan's posts on debugging. Second is David Agans' book Debugging, which I really like as an introduction, so much that I bought a bunch of copies to give as gifts to early-career friends.

On top of what they say, here's one technique I like: you can speed up debugging by asking broader questions.

Debugging as hypothesis building

I've tried to write a blog post on tag systems for years now. Literally years, I think I first started drafting it out in 2018 or so? The problem is that there's just so much to them, so many different approaches and models and concerns that trying to be comprehensive and rigorous is an exercise in madness.

So screw it. These are my noncomprehensive, poorly-researched thoughts on tag systems, thrown on the newsletter. This is not about implementation of tag systems, just their design.

What is a Tag

A tag is a metadata label associated with content. The tag name is also the id: two tags with the same name are the same tag. Tags appear in almost all large systems:

Lots of admin stuff today! First, we have a new blogpost, the full version of the complexity preview I shared last week. I'm also announcing a new TLA+ workshop! Or more precisely, three workshops. To make it easier on people's schedules, there are three dates you can sign up for: March 20, May 15, and June 12. And there's no fee to move between classes if something comes up and you can't make your session. Use the code C0MPUT3RTHINGS for 15% off..¹

Anyway, on to the main thing. A couple of years ago I started work on a Logic for Programmers pamphlet, then ADDed into some other project. I started work on it again last week with the hope (the hope) of having an early version available by the end of winter. I'm writing the book in Sphinx but compiling it to LaTeX and then a pdf. I like using Sphinx because it's (relatively) easy to create "directives", or new types of content with special processing rules.

The main technical challenge so far has been making an "exercises" directive. The pamphlet will have a lot of exercises. I want solutions to automatically be placed in the back of the book, and I want exercises and solutions to hyperlink to each other.² So I need to turn this:

.. exercise:: Implication
  :name: impl-1

  My Exercise!

  .. sol::

    My Solution!

One of the weirdest and most wonderful things about people is that they can make a joke out of anything. For any human discipline there's people making jokes about that discipline. In programming, that starts with memes like "how do I exit vim" (as typified in places like r/programmerhumor), or funny examples of awful code (such as from TheDailyWTF).¹

Those are both highly accessible kinds of jokes. More interesting to me is the humor that heavily rely on experience or background knowledge, where the expectation is that many people won't have the context that makes it funny. This is comedy that is produced by programmers for programmers. By relying on the shared context of software engineering, the gags aren't recognizable as mainstream jokes. You could easily explain why this is a joke to a normie, but could you explain Enterprise Fizzbuzz? Aphyr's Technical Interview series?

(This is something that happens in all fields, not just programming. 441 is a hilarious juggling pattern.)

The most interesting is when the medium of programming is itself used as a comedy substrate. This would be something like vanillaJS. There's also some cases where the joke is an entire programming language. Not many, since making a PL is hard, but a few!

I've recently been real fascinated by the topic of complexity and what keeps us from keeping software simple. The wider net likes to blame "lazy programmers" and "evil managers" for this, as if any software could, with sufficient time, be made as simple as "hello world". I've instead been looking at how various factors create complexity "pressure". Code that needs to satisfy a physical constraint is more likely to be complex than code that doesn't, etc.

One complexity pressure is "impedance": when the problem you are solving isn't well suited for the means you have to solve it. For example, if you need to write really fast software, then Python will be too slow. You can get around this by using foreign function interface, as scientific libraries do, or running multiple processes, as webdevs do, but these are solutions you might not need if you were using a faster language in the first place. In a sense impedance is complexity that comes from using "the wrong tool for the job."

Saying that python is the "wrong tool" for data science is a little inflammatory. It might have impedance flaws, but it also has a lot going for it— rapid prototyping, a huge community, a large ecosystem, etc. Surely those matter more than the added complexity of slowness!

More broadly, "use the right tool for the job" directly contradicts the best practice of choose boring technology: