Archive

I’m a pretty gullible person.

When I was a kid, my sister told me that there was a monster inside the toilet. For years after I’d flush and then run out of the bathroom in panic. As a teen, I discovered the James Randi forums and immediately became a true believer in the power of skepticism.¹ Skepticism is great! It’ll keep me from falling for flimflam anymore. If I follow the principles of skepticism then people will stop thinking I’m gullible. Hooray!

In other words, I was gullible enough to believe in the skepticism ideal instead of the Skepticism identity. You’re only supposed to be skeptical of what the community considered valid targets. Like if somebody pulls out a paper disproving astrology, you shouldn’t then point out that the researcher screwed up their χ² test and also was later caught fabricating data. Stuff that debunked pseudoscience was allowed to be “sloppier” because it served the Skeptic mission.

It was only years later that I realized I was doing skepticism wrong, but by that point the damage had been done. I fell for the ideals so wholeheartedly they became principles: spreading misinformation is wrong and debunking it is virtuous, regardless of what the misinfo is. Turns out this is really hard to do! We’re much better at seeing flaws in positions we disagree with than positions we like. It’s just part of human nature to be easier on “our side”.

In Superintelligence: The Idea That Eats Smart People, Maciej Pinboard nee Cegłowski talks about analyzing AI risk with the perspective of the “outside view”:

Say that some people show up at your front door one day wearing funny robes, asking you if you will join their movement. They believe that a UFO is going to visit Earth two years from now, and it is our task to prepare humanity for the Great Upbeaming. […] The outside view tells you something different. These people are wearing funny robes and beads, they live in a remote compound, and they speak in unison in a really creepy way. Even though their arguments are irrefutable, everything in your experience tells you you’re dealing with a cult.

Of course, they have a brilliant argument for why you should ignore those instincts, but that’s the inside view talking. […] The outside view doesn’t care about content, it sees the form and the context, and it doesn’t look good.

This is one of the most powerful tools in doing research. Analyzing the technical merits of a practice, or technology, or $THING is really hard. Ideally we’d give everything we explore a fair shake, but we have limited time and need heuristics to decide what to spend time on. If something fails the outside view, then we can probably skip it without investigating it further.

What does the outside view look like in software? In my experience, here are a few red flags:

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:

First some good personal news: I did a hiatus over the summer due to severe depression issues. Well, I finally got into an intensive outpatient program, which so far seems to be helping, and I’m optimistic it’ll leave me in a better place longterm.

Now some bad professional news: IOPs are both really time-consuming and mentally exhausting, which makes it hard to do more than my core client work. Don’t get me wrong, I want to write and I have the capacity to write, but there’s also a ton of research, synthesis, and editing that goes into the usual blogposts and newsletters. That’s why the last newsletter was pretty off-the-cuff opinions— it’s a lot less mental overhead.

So this week I’ll do another low-stress thing and provide short answers to several topics. Specifically, these topics:

New Post: ADTs in TLA+

Using Abstract Data Types in TLA+. It’s an adaptation of part of my TLAConf talk. It’s also a lot more advanced than most of the material I put online, and I expect it to only be useful to experienced TLA+ users. But that stuff is important, too. The community has made a lot of improvements in beginner-level instruction, so now there’s more of an audience for advanced techniques. I want those people to keep learning, too.

I don’t really have a formalized theory of the impact of “skill ceilings”, but I want to think they’re bad. In particular I’m pretty jealous of the Haskell community, which is really good at forever raising the skill ceiling. You can argue they don’t give enough priority to beginners and intermediates, and I think that’s a fair critique, but I also believe they do a much better job of pushing the boundaries of their world than other language commuities do. And I want that in formal methods, too.

See also: Blub Studies.

I know I said no newsletter this week but this just hit me and it’s small enough to write up so I’m fitting it in. The Monty Hall problem is a famous probability puzzle. From Wikipedia:

Suppose you’re on a game show, and you’re given the choice of three doors: Behind one door is a car; behind the others, goats. You pick a door, say No. 1, and the host, who knows what’s behind the doors, opens another door, say No. 2, which has a goat. He then says to you, “Do you want to pick door No. 3?” Is it to your advantage to switch your choice?

Most people say it doesn’t matter, that regardless of if you switch or not you have a 50% chance of getting the car. But switching actually wins 2/3rds of the time!

I’ve never been satisfied with the many, many explanations I’ve read. I get the math, but every explanation feels like a sleight-of-mind, where if you poke just a little bit it’ll all fall apart. The other day I came up with a variation:

Read it here! https://www.hillelwayne.com/post/alloy6/

Features my first attempts at using vector graphic diagrams to explain things better, like this:

Reminder, no newsletter next week due to workshop. See you all December 13!

My job these days is researching exotic software technologies and selling them to companies, which means I’m a software evangelist. And because I literally cannot turn my brain off ever, I started thinking about what “evangelism” actually means.

Evangelism is an “embarrassing job”: SE culture looks down on evangelism, considering it untrustworthy. I’m not doubting the valid reasons. I’m lamenting that there’s no community to discuss the techniques of evangelism, because the internet would gleefully tear it to shreds.¹

(I mean, beyond the usual clickfarm junk which I have notorious opinions about)

So a couple of weeks ago I wrote Finding Alloy’s Niche, where I said I wasn’t expecting the new Alloy 6 release to change all that much. It came out last Tuesday, I tried it out, figuring that I’d update the Alloydocs in mid-December or so.

Totally unrelated: I was planning on uploading a TLA+ post to the blog today, it’s 99% finished, but I didn’t bother because I need to get an Alloy post out right frickin’ now.¹ Because as of last Tuesday all existing Alloy learning material is obsolete.

The online tutorial uses signature cloning and state signatures to emulate a temporal spec. Every example in Daniel Jackson’s book at some point has to emulate time. The Alloydocs has an entire section on ways to represent time. Alloy material breaks down to “various tricks to hack time into your spec” and “everything else”. But now Alloy 6 has first class time constructs. Instead of writing the river crossing puzzle like this:

-- fox/chicken/corn puzzle
-- from sample modules
module examples/tutorial/farmer

open util/ordering[State] as ord

abstract sig Object { eats: set Object }
one sig Farmer, Fox, Chicken, Grain extends Object {}

fact eating { eats = Fox->Chicken + Chicken->Grain }

sig State {
   near: set Object,
   far: set Object
}

fact initialState {
   let s0 = ord/first |
     s0.near = Object && no s0.far
}

pred crossRiver [from, from", to, to": set Object] {
   // either the Farmer takes no items
   (from" = from - Farmer - from".eats and
    to" = to + Farmer) or
    // or the Farmer takes one item
    (one x : from - Farmer | {
       from" = from - Farmer - x - from".eats
       to" = to + Farmer + x })
}

fact stateTransition {
  all s: State, s": ord/next[s] {
    Farmer in s.near =>
      crossRiver[s.near, s".near, s.far, s".far] else
      crossRiver[s.far, s".far, s.near, s".near]
  }
}

pred solvePuzzle {
    ord/last.far = Object
}

run solvePuzzle for 8 State

assert NoQuantumObjects {
   no s : State | some x : Object | x in s.near and x in s.far
}

check NoQuantumObjects for 8 State

A year or so back I wrote the newsletter post Don’t use Markdown for documentation, where I complained about its lack of extensibility and cross-project referencing. People’s critique fell along two lines:

1. “Everybody on the team already knows and is willing to write markdown”: fair enough— I mostly care about dense, complex technical writing by an enthusiastic writer. If you need everybody to pitch in, you shouldn’t force them to learn a completely new technology.

(This gets a little rambly, I’m trying to figure out some stuff and thought it’d be nice to share my thinking process.)

I’ve been thinking a lot about Alloy lately.

(If you don’t know about Alloy, It’s another formal specification language. I have an introduction .) Partially due to a work thing, partially due to the upcoming Alloy 6 release, and partially because I just haven’t given it as much attention as I’d like. TLA+ is a lot more popular than Alloy, mostly because I’ve spent a lot more time TLA+. But also because Alloy’s use-cases are less obvious than TLA+’s.

Sup nerds!

Last week the SPLASH conference— the main academic conference for programming language research— came to town. I decided on a whim to buy a ticket and go.

One of the weirdest things about software engineering is how many people hate comments.

Like actually . There are influential people out there who say that if comments are a sign your code is bad, because you failed to make your code understandable enough to not comments. Comments lie and go out of date, they say, code is the only source of truth. Instead, you should have , where good variable names and code organization make comments superfluous. People can learn what the code does just by reading the code! Then you don’t need comments, except for very rare exceptions.

So my TLAConf talk is out and I was talk about technique research but then I saw this tweet and knew I had to rant about it:

New Essay: How to Solve the Sudoku Puzzle with programming

New essay up! How to Solve the Sudoku Puzzle with programming. This one is a little conceptual, so you might want to read it before the rest of this newsletter. Spoilers below!

Sup nerds, I’m back from Strange Loop! I have a million ideas I want to write about now, but I’ll stick to one of the lighter, sillier ones. Based on a claim by (I think) Jess Kerr, who said something like “In domain-driven design, you’re supposed to start with concrete examples, because those flush out the edge cases of your problem domain.”

And you know what’s the best edge case?

I’m preparing my talk for the TLA+ Conference this week. I asked around about intermediate stuff people wanted me to cover and there was a lot of interest in model optimization. The TLA+ model checker, TLC, brute forces every possible reachable state. If there are lots of possible states then it’ll take a very long time to run. The fundamental skill of optimization is being able to estimate how many states there are and how many states a safe change will eliminate.¹

There’s a connection to another field of verification: property-based testing! In PBT you take input generators and run them through tests. For example, you might generate random lists of up to five integers, where each integer is between -10 and 9. If the sample space is too big, most inputs will be uninteresting. Part of getting better PBT coverage is estimating how many inputs there are and how many a safe change will eliminate. There’s similar connections to simulations and constraint solving, where things are “slow” for related reasons.

Over the weekend, I read the question Is the Formal Methods Winter About to End on Lobsters:

Formal methods (theorem proving, model checking, static analysis, abstract interpretation, advanced type systems, program semantics, etc) have remained a relatively niche topic during the last two and a half decades. The field saw much interest during the 1980s and early 1990s. Tony Hoare’s 1996 speech recognized formal methods were so far unable to scale to real-world software, and that event perhaps marked the beginning of a formal methods winter. [\n] Do you think the field is starting to regain attention?

Hey nerds, I’m back! Still not all that recovered from mental health garbage, but turns out writing is a big part of my mental health, so stopping that for a while was a bad idea. Gonna ease back into things, which means this newsletter will be a lighter write. That’s right, it’s time for a recommendation!

How ACOUP made me a better programmer

There’s this blog A Collection of Unmitigated Pedantry, by Bret Devereaux, about nerd culture and military history. It has nothing whatsoever to do with programming. My first exposure was his demolishing the myths that Spartans had in any way an admirable society or were particularly good at fighting. From then on I was hooked.

Hi everyone,

My depression has gotten a lot worse in the past month and it’s seriously disrupted my ability to work. I’m taking steps to handle it, but in the meantime, I also need to cut down on non-essential work. That means prioritizing bill-paying content over passion projects like the newsletter.

I’m hoping to start writing Computer Things again by September and am confident it’ll be back by October at the latest. I still want to write, I just have reduced capacity for now.

I’m finally (finally!) working on a new version of the Are We Really Engineers talk, which has got me once again thinking about the differences between “Programming” and “Software Engineering”. I’ve also been wholly physically and mentally consumed last week by the art machine:

A while back I got really into “corporate blogs”. Why are they so soulless? Why do they all sound the same? I asked a friend had managed one of these blogs, and she told me it was all SEO. It’s written to trick Google’s Algorithm into ranking the root domain higher.

Yesterday I saw this tweet:¹

I’m a big advocate of Empirical Software Engineering. I wrote a talk on it. I wrote a 6000-word post covering one controversy. I spend a lot of time reading papers and talking to software researchers. ESE matters a lot to me.

I’m also a big advocate of (FM). I , I’m helping run a conference on it, I . There’s almost no empirical evidence that FM helps us deliver software cheaper, because it’s such a niche field and nobody’s really studied it. But we can study a simpler claim: does catching software defects earlier in the project life cycle reduce the cost of fixing bugs? Someone asked me just that.

Okay so let’s say I have a function f and ask you to figure out what it is. Input’s a list of integers, output is one integer. You gotta figure it out by seeing what inputs give you what.

First test: f([3]) == 3. This removes some possibilities, like , but there’s still a lot of other possible functions. It could be , it could be , or , or or or . It could even be the constant function . You can think of these all as a of sorts, the set of all functions that . There’s a lot of programs in this space, and they’re all very different, so we know our spec is too loose.

Whole lotta talk about formal methods last week. Moshe Vardi dropped an ACM piece, Jean Yang wrote an essay, and Nicholas Tietz-Sokolsky frontpaged Hacker News. I missed most of these as they happened because working on important consulting stuff. Looking back at the discussions, though, I saw a lot of the usual misconceptions people have about formal methods. It’s a very interesting and important field, but not one that programmers are familiar with, and that leads to a lot of misunderstandings. This is an attempt to address some of these. Disclaimer, I specialize in a couple of these tools, but believe I have enough familiarity with the rest to present them accurately.

What is a specification?

The most popular testing library in Ruby is called RSpec, and uses the terminology of Behavior-Driven Development, where tests are called “specifications”. My first ever talk about TLA+, “your tests are not your specs”, is about how this terminology is all wrong and we should reserve “specification” for formal methods. People seemed to enjoy the talk, which gave me the confidence to apply to Strange Loop, which I launched into a book deal, and now I do this for a living.

There’s nothing I’m rarin’ to share so I figured I’d talk about a concept in verification I see a lot but haven’t seen explicitly discussed anywhere. I don’t think this is revolutionary or anything but you might find it a useful heuristic.

There are two kinds of time in a system. The first is physical time, which is what most people think of as “time”. Physical time is duration something takes to run. is the abstract division of the system into epochs. A system belongs to two separate epochs if there’s a “before” and “after” that occupy different places in the state space. That means there is some query that returns different results for the same parameters. Usually physical and logical time are correlated, but not always:

People say “comment the why, not the what”, the idea being that the code should be self-documenting and the comments should only be a last resort for explaining stuff. Comments can get out of sync, but the code is always the code, so there’s no need for unnecessary redundancy.

I disagree: No matter how self-documenting the code is, comments help a lot with understanding stuff. Whenever I go back to an old project, I find the comments far more useful to reorient myself than my code or my tests. Here are some cases where adding the “what” is really helpful.

Providing Context

One reason I like teaching is it helps me understand things better. This came up in a couple different ways while working on the new book, and I’m too delighted by it not to share. Say we have the following user requirements:

Our conference center has a bunch of rooms that are reserved by people each day. Each room has a set of time slots that can be reserved. We need software that supports this.

That gives us three domain objects, , , and (time), and the concept of . But there are many different ways our software could reservations:

New Post: Clever vs Insightful Code

I shared an early version with the newsletter some time back, and now the final version is done! This one is less technical than usual, just me trying to a difference between different classes of “cleverness” in programming. I think lumping them all under the same brush does us a disservice, and I figure calling out the differences can lead other people to do more interesting stuff with the division. Enjoy the blog!

May is finally, finally over. This was one of the roughest months both jobwise and lifewise in recent memory. But now all my deadlines are over, I’m fully vaxxed, and I finally have time to start writing again. It might take me a while to get things back on track again, but at the very least I’ll be back to sending newsletters (at least) weekly.

So I’ve got a big project for June:

Predicate Logic For Programmers

I’m in the process of updating my TLA+ workshop for my class next week.¹ Every time I run it I get new ideas on what to improve. After April’s class, one of the most important changes I noticed was also one of the smallest. In TLA+, there’s two ways to write “not-equals”: # and . I’m used to writing and find really weird, so I teach . After April, I mass changed every to .

No Newsletter Next Week

I hate to do this twice in three weeks, but I have a TLA+ workshop next Monday.

A Brief Introduction to Esolangs

pieces of content for you!

No Newsletter next week

I have some real life stuff going on and also a secret project deadline. I’d still like to make time for the newsletter, but it’s easier to just say it probably won’t happen. Sorry.

Esolangs!

Last Tuesday’s piece Why UML “Really” Died went viral. I’m glad that people enjoyed it, and I also was happy to use all that fallow research, but something’s been bothering me. People didn’t switch from UML to something else; they walked away from the mindset entirely. UML wasn’t fulfilling a meaningful use case for programmers, so when it didn’t work they didn’t look for an alternative. The last five years of my life have been dominated by an “alternative”: formal methods. I teach people how to write blueprints of a system in TLA+ or Alloy.¹ Why should I believe that formal methods will succeed where UML failed?

May TLA+ Workshop

Just one slot left! May 24-26. Learn how to find bugs that would slip right past types, test, and code review. Also surprisingly pertinent to this week’s newsletter!

Donations

I have a love-hate relationship with APLs. On one hand, they’re unbelievably powerful in what they can do. On the other hand, they’re absolutely awful in what they can’t do. I always feel like I’m walking that thin line between brilliant and stupid.

For those you who don’t know APL is one of those array languages, notorious for all its funny characters:

New Essay: Why Specifications Don’t Compose

Read it here! Didn’t sneak peek it to the newsletter because I used a lot of Hugo preprocessing, so this is the first time y’all are seeing it. !

“Keep it simple!” “Just write simple code!” “Great devs come up with simple solutions!”

I get it. Simple code is better than complex code. It’s an important lesson, and I’ll admit that it’s one we easily lose sight of, and a lot of code is more complicated than it needs to be. But weirdly enough, no matter how many times people say “write simple code”, no matter how many times we repeat our mantras, a whole lot of software is really complicated! Why is that? Why can’t we write simple code? If you look online you’ll run into shit like this:

May TLA+ Workshop

Still three slots left! May 24-26. Learn how to find bugs that would slip right past types, test, and code review.

No Newsletter Next Week

I intended this newsletter to be my thoughts without editing, and I have a new thought, so here goes. I want to respond to this discussion:

TLA+ Workshop

You know the drill. TLA+ Workshop, three days, May 24-26. Only four slots, so sign up before they’re gone!

New Essay

This is a little out of the normal for this newsletter but I had an idea that I just needed to get off my brain. This is going to be a little more free-association than the usual posts. There will be a normal newsletter on Monday.

So there are lots of antipatterns, right? God objects, balls of mud, global variables. Why are these things antipatterns? Because they’re easy to do and common but cause headaches down the line. What kinds of headaches? They make changes harder, bugs sneakier, communication more difficult. This assumes a couple properties of the code:

• There is (or will be) lots of code

1.

A joke I once read:

TLA+ Workshop

Only one slot left! 3 days, April 12-14. Register here!

Why Don’t Specs Compose?

New TLA+ Workshop

3 days, April 12-14. Register here!

Vim is Turing-Complete

This is a weirder theorycrafting post and I don’t know how much I actually believe in it, but it seems like something you all’d enjoy reading.

A couple weeks back I was trying out Semgrep, a static analysis tool that matches the structure of the code you’re writing. For example, write to match all statements in Python, even aliased ones. Then you could write a rule saying to raise errors if it finds that. The rule file would look like this:

Hello everyone!

First of all, new post: TLA+ Action Properties. It’s about specification properties on to the state, not just properties 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 is true.” It’s a really powerful modeling technique that makes TLA+ a lot more expressive. Check it out!

Talk Tuesday

I’m speaking at Berlin Function Programming Group! Noon CST tomorrow, register here. It’s my standard TLA+ talk, so there won’t be any major surprises if you’ve heard a version of it before. Still, if you haven’t, here’s your chance :)

New Schedule

It’s been a while! Let’s just say the past couple of weeks have not been kind to me and leave it at that.

So, newsletter. I got 40% through writing about book recommendations, then read Why Is Naming Things Hard? and threw it all out to talk about naming things instead. So let’s talk about naming things!