Computer Things

Logic for Programmers is now in Beta! v0.5 marks the official end of alpha! With the new version, all of the content I wanted to put in the book is now present, and all that's left is copyediting, proofreading, and formatting. Which will probably take as long as it took to actually write the book. You can see the release notes on the leanpub...

Sup nerds, I'm back from SREcon! I had a blast, despite knowing nothing about site reliability engineering and being way over my head in half the talks. I'm trying to catch up on The Book and contract work now so I'll do something silly here: ternary operators. Almost all operations on values in programming languages fall into one of three...

No Newsletter next week I'll be speaking at USENIX SRECon! TLA from first principles I'm working on v0.5 of Logic for Programmers. In the process of revising the "System Modeling" chapter, I stumbled on a great way to explain the temporal logic of actions that TLA+ is based on. I'm reproducing that bit here with some changes to fit the newsletter...

From Leslie Lamport's Specifying Systems: You should be suspicious if [the model checker] does not find a violation of a liveness property... you should also be suspicious if [it] finds no errors when checking safety properties. This is specifically in the context of model-checking a formal specification, but it's a widely applicable software...

Sorry there was no newsletter last week! I got COVID. Still got it, which is why this one's also short. Logic for Programmers v0.4 Now available! This version adds a chapter on TLA+, significantly expands the constraint solver chapter, and adds a "planner programming" section to the Logic Programming chapter. You can see the full release notes on...

(Feeling a little sick so this one will be short.) I'm often asked by clients to review their (usually TLA+) formal specifications. These specs are generally slower and more convoluted than an expert would write. I want to fix them up without changing the overall behavior of the spec or introducing subtle bugs. To do this, I use a rather lovely...

Blog Hiatus You might have noticed I haven't been updating my website. I haven't even looked at any of my drafts for the past three months. All that time is instead going into Logic for Programmers. I'll get back to the site when that's done or in 2025, whichever comes first. Newsletter and Patreon will still get regular updates. (As a...

Logic For Programmers v0.3 Now available! It's a light release as I learn more about formatting a nice-looking book. You can see some of the differences between v2 and v3 here. Why Not Comments Code is written in a structured machine language, comments are written in an expressive human language. The "human language" bit makes comments more...

Last week Leslie Lamport posted The Future of TLA+, saying "the future of TLA+ is in the hands of the TLA+ foundation". Lamport released TLA+ in 1999 and shepherded its development for the past 25 years. Transferring ownership of TLA+ to the official foundation has been in the works for a while now, and now it's time. In the document, Lamport...

Time is state Imagine I put an ordinary ticking quartz clock in an empty room. I walk in, and ten minutes later I walk out with two photograph prints.1 In the 1st one, the second hand is pointing at the top of the clock, in the 2nd it's pointing at the bottom. Are these two copies of the same photo, or are they two different pictures? There's...

I was recently commissioned by a company to make a bespoke TLA+ workshop with a strong emphasis on reading specifications. I normally emphasize writing specs, so this one will need a different approach. While working on it, I had an idea that might make teaching TLA+— and other formal methods— a little easier. Pseudospecs There are two problems...

I make a lot of personal software tools. One of these is "texttools.py", which is easiest to explain with an image: Paste text in the top box, choose a transform, output appears in the bottom box. I can already do most of these transformations in vim, or with one of the many online tools out there, but I prefer my script for two reasons:...

I just published a new version of Logic for Programmers! v0.2 has epub support, content on constraint solving and formal specification, and more! Get it here. This is my second book written with Sphinx, after the new Learn TLA+. Sphinx uses a peculiar markup called reStructured Text (rST), which has a steeper learning curve than markdown. I only...

Last Friday CrowdStrike did something really bad and it destroyed every airport in the world. I didn't bother to learn anything else about it because I was too busy writing my 10k whitepaper about how all the problems were all caused by one simple mistake: not drinking my patented Miracle Tonic™®. Developers who drink my Miracle Tonic write code...

First of all, I wanted to extend a huge and heartfelt thank you to all of the people who bought Logic for Programmers. Seeing the interest is incredible motivation to continue improving it. If you read it and have feedback, please share it with me! Second, I have a new blogpost out: Toolbox Languages. It's about five obscure languages I use that...

I am delighted to announce that Logic for Programmers is now available for purchase! While still in early access, it's almost 20,000 words, has 30 exercises, and covers a wide variety of logic applications: Property testing Functional correctness and contracts Formal verification Decision tables Database constraints Data modeling and alloy...

The deadline for the logic book is coming up! I'm hoping to have it ready for early access by either the end of this week or early next week. During a break on Monday I saw this interesting problem on Math Stack Exchange: Suppose that at the beginning there is a blank document, and a letter "a" is written in it. In the following steps, only the...

You've got a wall in your apartment and a couch. You measure the wall with a ruler and get 7 feet, then you measure the couch and get 7 feet. Can you fit the couch against that wall? Maybe. If the two measure is exactly 7 feet than sure, 7 ≤ 7. But you probably didn't line your measuring stick up perfectly with the couch, and also the stick...

I spent the early week recovering and the later week working on Logic for Programmers ([init] [update]) because I have a self-imposed deadline of mid-July, backed up by a $1000 toxx clause. Here's where I currently am: 1: The book is now 14k words. About 4k are "basics", covering propositional logic, predicate logic, and set theory. Another 1500...

Post here! It's a really advanced TLA+ technique that I'm sure will alienate 90% of my readers. Patreon here. Anyway, I'm off to get a bone graft. Proper newsletter will come later this week when I've got more time to write.

Just an unordered collections of thoughts on this. In programming languages, nondeterminism tends to come from randomness, concurrency, or external forces (like user input or other systems). In specification languages, we also have nondeterminism as a means of abstraction. Say we're checking if a user submitted the correct password. A software...

Sup nerds, I'm back from DDD Europe! Still processing the conference and adjusting to the horrible jetlag but also itching to get writing again, so let's go. The opening keynote to the conference was called "Modern Tradeoff Analysis for Software Architecture". It was mostly about the factors that went into whether you should split up services...

No Newsletter next week I'll be giving my conference talk at DDD Europe. NoCode Will Not Bring Computing to the Masses I don't have a whole lot of time this week so here's something that's been on my mind a little. I haven't researched any of the factual claims; consider this more some incoherent early-stage theory. Define a "NoCode" tool as...

Behind on the talk and still reading a lot of research papers on empirical software engineering (ESE). Evaluating a paper studying software engineers is a slightly different skill than evaluating other kinds of CS papers, which feel a little closer to hard sciences or mathematics. So even people used to grinding through type theory or AI papers...

I'm speaking at DDD Europe about Empirical Software Engineering!1 I have complicated thoughts about ESE and foolishly decided to update my talk to cover studies on DDD, so I'm going to be spending a lot of time doing research. Newsletters for the next few weeks may be light. The other day I was catching myself up on the recent ABC conjecture...

New blog post! Software Friction is about how all the small issues we run into developing software cause us to miss deadlines, and how we can address some of them. Patreon here. "Integration tests" are just vibes You should write more unit tests than integration tests. You should write more integration tests than unit tests. "Integrated tests"...

Program testing can be used to show the presence of bugs, but never to show their absence! — Edgar Dijkstra, Notes on Structured Programming Dijkstra was famous for his spicy quips; he'd feel right at home on tech social media. He said things he knows aren't absolutely true but will get people listening to him. In the same essay he discusses how...

A lot of my formal specification projects involve concurrent or distributed system. That's in the sweet spot of "difficult to get right" and "severe costs to getting it wrong" that leads to people spending time and money on writing specifications. Given its relevance to my job, I spend an awful lot of time thinking about the nature of...

New Blogpost Don't let Alloy facts make your specs a fiction, about formal methods practices (and a lot of Alloy). Patreon link here. Some notes on for loops I sometimes like to sharpen the axe by looking at a basic programming concept and seeing what I can pull out. In this case, for loops. There are two basic forms of for loops: for(i = 0; i ...

Next week is April Cools! A bunch of tech bloggers will be writing about a bunch of non-tech topics. If you've got a blog come join us! You don't need to drive yourself crazy with a 3000-word hell essay, just write something fun and genuine and out of character for you. But I am writing a 3000-word hell essay, so I'll keep this one short. Last...

Whenever I talk about formal methods, I get the same question: Can I use the spec to generate my code? People are worried about two things. One, that they'll make a mistake implementing the specification and have bugs. Two, that over time the implementation will "drift" and people won't update the spec, leading to unexpected design issues. These...

Pairing is two people working together to write code, while mobbing is three or more. Pairing has been part of the programming milleau since at least the 90's (with extreme programming), while mobbing is more of a 10's thing. I'm going to use them interchangeably from here on out even though they're not interchangeable, because I think everything...