Archive

tl;dr: online TLA+ manual/advanced techniques/examples here.

TLA+ is a tool for testing abstract software designs. I first stumbled on it in 2016 and found it so useful I wrote a free online guide to help others learn it. Then I decided the guide wasn’t good enough and wrote Practical TLA+ in 2018. Then I decided the book wasn’t good enough and needed a second edition.

Just kidding! Book’s never getting a second edition, because it costs $26 and no matter how good I make it, it’s never going to have the reach of a free resource. So instead I took all the teaching lessons I learned over the past four years and turned them on rewriting the online guide from scratch.

Six months and 40,000 words later, the Learn TLA+ rewrite is now online! While I’m nowhere near done writing, the guide’s now complete enough to be a useful TLA+ resource, for beginners and experts alike.

Fifteen days left

Hi everyone! Been a couple of weeks since the last email. As mentioned, I took June off from weekly newsletter to work on the new version of the learntla web site. I have a requirement to have a version I’m happy uploading by the end of June, or else I owe a random one of you a thousand dollars. That’s just two weeks away, and I figure I should update everyone on how that’s coming so far.

Currently I’ve written about 28,000 words. That’s about twice the current version of learntla and about half the length of Practical TLA+. With the exception of the sections on Action Properties and pure TLA+, all of the core learning material is in “polish mode”. Action Props are about 60% done, pure TLA+ is maybe 30% done. I also need to take a lot more screenshots and make a lot more diagrams— dreary work, but easy enough to do.

In addition to core material, I’m writing a bunch of special topic essays. Here’s the stuff I want in the MVP:

Hey everyone!

We gotta start with some housekeeping. First, you might have noticed that the newsletter email’s changed. Several people informed me that Gmail was sending the newsletter to spam and Buttondown suggested I send from a custom domain to fix it. There shouldn’t be any changes needed on your end, though if you have message filters you might need to update them. And you can still email support@buttondown.email if you see any issues.

Second, registration for the TLA+ conference is now available! Register here. I’m teaching this year’s TLA+ preconf workshop with an attendee cap of thirty. For the record, my usual cap is four. God help me.

Finally, this is the last weekly newsletter until July. I’m teaching a TLA+ workshop next week, and after that I’ve got to go all in on the learntla June deadline. I might do an off-the-cuff newsletter if something’s really stuck in my head but don’t expect anything. By July we’ll be back to at-least weekly as per usual.

Conventionally we communicate programming ideas with talks, papers, and blog posts. But we can also communicate ideas with entire codebases. If someone finds a security exploit, she’ll sometimes publish a proof of concept to prove the exploit isn’t just theoretical.

Now let’s say the exploit PoC comes with a ton of command-line flags: verbose mode, configuration options, output formats, the whole works. Now the writer is communicating something subtly different: not just that the exploit exists, but she wants you to experiment with it. She’s making it as easy as possible for you to play with the exploit yourself and come up with variations and consequences.

This makes codebases like any other kind of communication medium. There are different styles you can use to say subtly different things. There are also different “genres”, or overt things you use the codebase to say. Some examples:

Of Genres

This one’s going to be a bit off topic. I have a long piece on the history of pattern matching I want to do but this week is really tight work-wise and this one’s less time-intensive to write.

I’m very interested in “knacks”, or mental tricks that help out in day-to-day life. For example, being able to count quickly and having good memory palaces. Last year I thought I’d memorize a larger multiplication table. Sounds a bit silly, but I come across multiplications a lot, and knowing a large table makes it faster. Like what is 8 feet in inches? Most Americans are only taught the 9x9 table, so they’d have to do 8×10 + 8×2. But some kids are taught the 12x12 table, so they just know that 8×12 = 96.

So there’s clearly some value to knowing a larger table, as it means you can do more stuff in your head, instead of needing a calculator. The only reason we stop at 9x9 (or 12x12) is because you can only do so much with kids before they lose interest. But as an adult I’m willing to put the time in to multiply better. Why not memorize the 99x99 table? Then I can see, say, 14×87 and instantly know it’s 1218.¹

One teensy tiny problem: multiplication tables scale quadratically. The 9x9 multiplication table has 45 terms.² The 99x99 table has 4950. I’m willing to put time into this project, but not that much time.

As a teen I regularly read The Daily WTF, a comedy site about bad programming and bad software jobs. Two articles have stuck with me. The first is this fantastic article about an incredibly wtf radio jammer. The second is No, We Need a Neural Network, which opens with this:

M.A. is one of the world’s foremost experts on neural networks. His undergraduate specialty was artificial intelligence, his master’s thesis was about genetic algorithms, and his doctoral dissertation covered evolutionary programming. Such an extensive computer science education opened up a wide range of career options, ranging from a professor at a university to … a professor at another university.

The article was published in December 2006. Within six months NVIDIA released CUDA, by 2009 Raina et al were training neural networks on GPUs, and in 2012 the GPU-trained AlexNet crushed every single image recognition benchmark. It took just over five years for neural networks to go from punchline to multibillion dollar industry.

I think about that a lot.

Hey everyone!

I realize I should give you all an update on the current learntla progress! So first of all, I’ve been continuously pushing my work to the learntla-v2 repo. Every push also builds the virtualenv as the artifact, so if you want to see the current state of the documentation, you can clone the repo, download the venv, and then run venv/bin/sphinx-build to get a local copy.

Currently I’m 15,000 words in and expect to have the first public version ready by the end of June. To keep myself to that schedule I set up a toxx clause: If I miss the deadline I’ll pay $1000 to a random newsletter subscriber. That public version won’t be the intended final version, just the minimal content I’d be happy with. In particular, to cut scope I’m leaving out all exercises.

v2 is organized slightly differently from v1 and Practical TLA+. In addition to reordering the content (constants now come much earlier, and nondeterminism comes after functions), I’m splitting examples up into simple “in-band” ones that are inline with the teaching material and complex “out-of-band” ones that are on separate (linked) pages. That way I can separate “examples for showing the concepts in use” from “examples for learning how to specify better”. Also, I reuse the same problem for the in-band examples. Currently, the two main in-band examples are “checking if a string contains duplicates” and “threads incrementing a counter”, though there are a couple others, too. The out-of-band examples are going to be more diverse. None of those are written yet, but the ones I plan to do are (at the very least):

I am really, really into cooking. In the heady days of 2016 I regularly threw dinner parties for 30+ people. These days I don’t hate myself that much, but it’s still a big part of my life. I know more about my city’s best grocery stores than its best restaurants and regularly bring homemade candy to conferences. I really like cooking.

In order to cook well, you need to practice mise en place: prepping all your ingredients before you start cooking. If you have to chop and sear three types of vegetables, first you get them all out and washed, then you chop them all, then you sear them. You don’t start prepping one vegetable while another is already cooking.

You can think of it as organizing your cooking workflow so that tasks are separated into “low-intensity” preparation and “high-intensity” work, where you’re bound by focus and tight timing. Without mise en place you’re doing the easy prep at the same time as the hard work, which makes everything more stressful and mistakes more likely.

How can we apply mise en place to programming? The most straightforward translation is doing all the project infra work before writing the code, but I don’t think that’s always appropriate. Software is different from cooking; the task is unbound and your requirements change. It doesn’t make sense to do a lot of prep that may be unnecessary.

(Sorry this is late! Dealing with COVID.)

I have mild ADHD. I can focus on strenuous mental tasks, but I can’t handle boring or repetitive work. Even something like “manually navigating to a folder” is enough to make procrastinate. I’m always looking for ways to aggressively optimize my workflow.

For example, one thing I have to do a lot is type my address into emails and chats and the like. For most people that isn’t a big deal, but for me it’s disruptive. One tool I use, AutoHotKey,¹ has “hotstrings”: if you type a hotstring, it replaces the text with a substitute.

::;adr::{My address}

I work with a lot of really esoteric technologies, like TLA+, Alloy, J, MiniZinc, and PRISM. Pretty much every non-mainstream technology has a “literature gap” between beginner and expert work.

Take J. If you go around the internet, you’ll find lots of articles extolling the virtue of array-based programming and a lot of experts showcasing the cool things you can do with J mastery.¹ Here’s what you won’t find:

• The best way to structure your code
• Common troubleshooting issues and how to get around them
• Common antipatterns
• Program dissections
• A well-organized documentation of the standard library with examples²
• Blog posts of people discussing techniques without needing to introduce basic concepts first

In other words, there’s material to get you started, and material for experts to share with other experts, but nothing for people to go from knowing the language to being a competent practitioner (CP). I’m using J as an example here, but almost all esoteric technology I know about has the same problem. This points to a user gap, where most of the users are beginners or experts. Experts don’t need to talk about this stuff because they already know it, so it’s not interesting to them. And beginners don’t know enough to talk about it usefully.

Hello everyone!

So first of all, new post. It’s about how I got into microscopy and a bunch of pictures I took that I like. It has nothing to do with tech at all!

…Some explanation is in order.

So, it’s also April 1st today, and that means the internet has to deal with the dreaded “April Fools” plague. The one day it’s socially acceptable for Serious People to do something silly, but Seriously. So you get one of two things:

The “iron triangle” of project management is “Cheap, fast, good: choose two”. This works on the assumption that quality is a metric while time and money are fungible constraints. We can exchange between time and money, and also lower our quality goals to require less of both. Then by LeMond’s law¹, if you aren’t using much of your resources, you can afford to be more ambitious and put yourself in a place that does demand more from your resources.

It occurs to me that we can flip “quality” around into a constraint by saying is a “shoddiness” is a quantity we can spend to make the product worse. Then time, money, and shoddiness become our three budgets that all work against each other— we can pay shoddiness and time to save money, etc. The three resources are also conceptually independent: most other resources we can think of (favors, scope) fall clearly into one bucket.

That got me wondering what the software iron triangle would look like. Not the development of software, which falls under project management, but the software itself. Are there fundamental constraints that act as universal conflicting budgets? I’m pretty sure I know what two of them are, but the third I’m more uncertain about. They are performance, complexity, and (possibly?) correctness.

Performance also includes other resources like memory or power-use, but the dominant resource in this budget is wall time. Most problems are solveable by brute force; we don’t do that because that’s an unacceptable performance cost. Over time computers become faster and we get more of this budget to work with, which leads to adages like “developer time is more important than CPU time”. But we don’t have an infinite budget, and it’s easy to waste too much of this resource if you’re not paying to it as a constraint.

The Problem

When teaching things I like to break code up into a set of small changes, showing the differences between each change. So if I start with

// version 1

boilerplate
more boilerplate
some code
more boilerplate

I’d show the next small change as a diff, like this:

Happy Pi Day!¹ To celebrate I want to get away from software for a bit and talk about something special. You may have heard the story that the Indiana legislature tried to change the value of π, to something like 3 or 4 or 3.15 or something like that. This is usually shared as evidence that Indianans are dumb hicks, but I don’t like leaving things at that. Why did they try to change π and what did they expect to happen?

I did the research, and now you get to hear the whole story. But to fully understand the context, I’ll need to explain math.

I’ll need to explain a lot of math.

Straightedge is for Squares

Hey y’all! Still hard at work on the new learntla version. It’s currently about a third of the length of original learntla, which is pretty impressive, given I’m estimating I’m like… 10% done with the first draft? At most. I’ve also written many of the tools I’ll need to manage the complexity of the larger docs, and specced out many of the examples and exercises I want to do.

By the way, we now have a TLA+ survey available! Please fill out the survey if you can, we really want to understand the community better, and this is a great way to give back! Click me click me click me

This is the third time I’m writing a TLA+ resource: the original learntla, Practical TLA+, and now this. Plus I’ve also done Alloy documentation and several workshops, so in all I’ve spent a lot of time in the past five years thinking about how to explain shit better. There’s a lot of stuff I didn’t know before that now feels so obvious! So obvious that it almost feels not worth talking about, but then again I didn’t know it before, so I’m guessing some of you don’t know it now. So I wanna share a short education concept I call “The Parable of the Crow”.

Specifically, this crow!

Last week I read Software I’m Thankful For and it inspired me to do a similar piece. I use a lot of different exotic tools, too, so I think it’s a good way to share some stuff most people haven’t seen. At least mainstream programmers, if you’ve been following me for a while a lot of this will be familiar.

TLA+ and Alloy

So let’s start with the big, obvious ones. TLA+ and Alloy are both formal methods languages for finding problems in designs. It’s something so outside the norm that many programmers don’t even know that directly testing designs is a thing that exists, much less that it’s economical and effective. I’ve met plenty of people who say FM couldn’t possibly work, and then after a five minute demo switch to “I need to learn this right goddamn now.”

That more than anything else is what makes me so optimistic about FM’s long term future. Most developers have a well-founded skepticism of new or exotic technology. So to see people get excited so quickly? There’s something really precious here.

First a term: by “treatise”, I’m not saying this newsletter is comprehensive, persuasive, or even correct. I’m using it to mean a very specific type of writing, one that presents an idea and its consequences without trying to convince people of that idea. I don’t even know if I’m convinced by the idea. I just want to see if I can communicate a specific idea, and if people understand it but reject it, I’m happy.¹

Consider we have a rectangle object:

class Rect():
    def __init__(self, l, w):
        self.l = l
        self.w = w

    @property
    def l(self):
        return self._l

    @property
    def w(self):
        return self._w

    @l.setter
    def l(self, _l):
        self._l = _l

    @w.setter
    def w(self, _w):
        self._w = _w

Website Haitus

Fortunately not depression this time, just a responsibility thing. From the announcement:

I’m not letting myself work on software content for the website until I finish both the Alloydocs update and the learntla rewrite.

(I’ll still be writing the weekly newsletter.)

Yeah, I’m incentivizing myself to write by rewarding myself with more writing. Hey if it works it works.

Once more: we are not modeling reality, but the way information about reality is processed, by people. — Bill Kent

I’ve got this working theory that you can tell how enthusiastic someone is about a subject by how obscure their favorite book is. It’s just a simple numbers game: there are more obscure books than popular books, so there are more obscure good books than popular good books, so the more books you read the more likely your favorite is an obscure one. In other words, if someone says they love fantasy novels and also their favorite novel is Harry Potter, odds are they don’t actually read that much fantasy.

I’m saying this because my favorite book on software is incredibly obscure, which must mean I’m a super cool software dude. That’s how logic works, right?

It’s Data and Reality, by Bill Kent. Unlike most books on data modeling, Data and Reality doesn’t tell you how to do anything, or give you advice on the best way to model. Instead, it’s a philosophical book on the nature of information and how we represent it. Kent doesn’t want you to follow his advice, he wants you to ask questions, to understand just what it is we’re trying to do. He opens the book with a whirlwind of examples where our intuition of meaning breaks down:

Some people, when confronted with a problem, think “I know, I’ll use regular expressions.” Then they solve their problem, hooray!

Regexes are great! I use them all the time! For some reason, though, people seem to hate them. And those “some reasons” are

1. They’re very hard to read, so you have no idea what a given regex you see does.
2. They’re fragile, so slight changes to the input can break your regex. Making them more robust also makes problem (1) worse.

This is usually in the context of putting a regex in your code, where it’s used to pull semantic information out of arbitrary texts. In that context, readability and robustness are really important. Simple regexes can work but for anything complicated you probably want to use a parser.

Hiya everyone! Workshop is all done and I’m alive again. For those of you just joining us, I teach formal methods workshops to companies. Working on a piece about my pedagogy now, actually; for such a large industry there’s surprisingly little shop-talk out there.

-

Okay so the last two newsletters were about research and the workshop was all formal methods, so let’s take a break from “stuff that pays the bills” and chat software philosophy for a bit. I recently read Improving end-to-end tests reliability. In order to make better E2E tests, they recommend building a lot of infrastructure to support the tests: high-level interfaces, automatic bisection, stuff like that.

This reminded me of a concept I’ve mentioned a few times before: software as an artifact. One of the fundamental differences between “programming” and “software engineering” is that engineering treats the software as an entity distinct from the thing it’s doing— as something that exists in its own right. The software has presence and needs to be supported as much as the client domain.

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: