Last week Boris Cherny, the inventor of Claude Code, mentioned that Opus was able to use TLA+ 1 to find race conditions in code. And now everybody on the internet is talking about formal verification. As a long-time educator ( 1 2 ) and advocate of TLA+, this is really exciting! TLA+ is great at designing complex concurrent systems and making sure they're bug-free. 2 As a long-time advocate of lev

Earlier this year I worked on a couple of AI-generated TLA+ specifications, and one thing I've noticed was that they all used the word "spine" somewhere. Then I saw some non-TLA+ public projects use "spine" too and got curious if it was a new LLMism (LLisM?). If it is, we should see it appear in a discontinuous jump in the number of code projects that use "spine". The proper way to thoroughly expl

Logic for Programmers has now been out for a month! To celebrate, I'm releasing the entire second chapter, "A Crash Course in Logic", for free on my blog. Read it here!

Newsletter updates were sporadic in July because of two weddings, two conferences (with two different talks!), and finishing Logic for Programmers . Huge thank you to everybody who bought a copy, as well as for your patience with the schedule. There's some podcast appearances, a conf talk, and a book sale at the end of this post. Newsletter updates will be sporadic in August because I just started

It's done. Logic for Programmers is now 1.0 and available in print. Full announcement here , official website here , direct Amazon link here . If you got an early version of the ebook, you can go back to leanpub to download the 1.0 for free. This marks the completion of a project that took five years of work, six bookwriting professionals, fourteen domain experts, and fifteen public alphas. This h

Between travel obligations and this last heads-down-gotta-get-the-book-done stretch I haven't had time to write any newsletters or even look at social media. The good news is that Logic for Programmers should be done and available in print hopefully in the next couple of weeks. Here's all of the printed proofs I've made so far: And here's what the current proof looks like on the inside: Looking go

There's a new release of Logic for Programmers ! This one, version 0.15, is the first true release candidate. There's a couple of minor touch-ups I need to do but all content is in and copy edited and proofread. Unless something absolutely major comes up, the next release will be 1.0 and available in print. Full release notes here . (I'm also testing if a smaller low margin PDF is better for phone

This is valid JSON: { "a" : 1 , "b" : 2 , "c" : 3 } This is invalid JSON: { "a" : 1 , "b" : 2 , "c" : 3 , } The difference is the last comma. The JSON grammar specifies that a comma can separate two members of an object but not postcede ("trail") a member. I think this was a design mistake. Say we want to add two new keys to the struct, one before the "a" member and one after the "c" member. Here'

So I said there wasn’t a proper newsletter this week, since I’m in Budapest prepping for a conference. But I still got a thing for y’all. There’s a lot of interesting topics I wanted to cover for Logic for Programmers , but the book is dense enough as it is and many of these were too tangential or technical to fit in well. So I’ve been writing some supplements and uploading them here . I’ve got fo

Short one this week because I'm way behind on book and conference prep. Last week a LinkedIn Influencer wrote about how math has nothing to do with programming, so I spite-wrote a rejoinder about how math is necessary to program (just try to write software without knowing arithmetic!) and man I forgot how much spite can fuel writing. Maybe I should go back to Twitter (absolutely not). But it got m

In some tests are stronger than others , I defined STRONG => WEAK to mean "any system passing test STRONG is also guaranteed to pass WEAK". This uses the logical implication operator, defined as P => Q = !P || (P && Q) . Implication may be the most overworked operator in logic. Among other things, it's also used in formal specification, where Spec => Prop means "any system satisfying Spec has prop

I'm in the middle of redoing the Logic for Programmers diagrams and this has surfaced a really annoying problem. The book is formatted in LaTeX using a pseudo-grid of 10.8pt × 7.2pt. The diagrams are done in Inkscape using a 10.8pt × 7.2pt. Last week I found out that these are not the same points. Latex defines a point as 1/72.27 inches (0.3515 millimeters). Inkscape instead uses 1/72 inches (0.35

So first the immediate news: I just released version 0.14 of Logic for Programmers ! This release is pretty similar to 0.13. There are a few rewrites but the vast majority of the changes are layout, copyediting, and technical editing. Full notes here . In related news, I've started doing test prints of the book: There's not a whole lot left to be done. I've gotta fix up some diagrams, do more form

An illegal state is a state we never want our system to be in. An unwanted state is a state we don't want to stay in. Many states that we wish were illegal are actually unwanted. Considering a calendaring software which stores calendar events as {user: {events: [event]}} , where each event has a start and end time. This allows one person to attend two events at the same time. We might consider thi

Take the following Python program: # x = 1, y = 2 x = 0 y = x print ([ x , y ]) It'll print [0, 0] . If we swapped the two assignments, it'd instead print [0, 1] . Each assignment happens in a separate temporal step. Pretty much all imperative languages behave this way. Now take the following TLA+ snippet: \* x = 1, y = 2 /\ x' = 0 /\ y' = x /\ PrintT(<<x', y'>>) This'll print <<0, 1>> . Unlike in

Sorry for missing last week! Was sick and then busy. This week I want to cover a pet peeve of mine, best seen in this comic: A "comprehensive and precise spec" is not necessarily code. A specification corresponds to a set of possible implementations, and code is a single implementation in that set. As long as the set has more than one element, there is a separation between the spec and the code. C

Happy April Cools! My not-tech post this year is Chicago vs New York Pizza is the Wrong Argument , which is mostly an excuse for me to talk about Chicago food. See here for all of the other April Cools submissions. As of this email we have sixteen posts; there's still time to submit something! 1 This one came out of a pizza argument with Marianne Bellotti , a true New Yorker who doesn't think deep

The famous article Choose Boring Technology lists two problems with using innovative technology: There are too many "unknown unknowns" in a new technology, whereas in boring technology the pitfalls are already well-known. Shiny tech has a maintenance burden that persist long after everybody has gotten bored with it. Both of these tie back to the idea that the main cost of technology is maintenance

No newsletter next week I'll be speaking at InfoQ London . But see below for a book giveaway! LLMs are bad at vibing specifications About a year ago I wrote AI is a gamechanger for TLA+ users , which argued that AI are a "specification force multiplier". That was written from the perspective an TLA+ expert using these tools. A full 4% of Github TLA+ specs now have the word "Claude" somewhere in th

Spinning a lot of plates this week so skipping the newsletter. As an apology, have ten free copies of Logic for Programmers . These five are available now. These five should be available at 10:30 AM CEST tomorrow, so people in Europe have a better chance of nabbing one. Nevermind Leanpub had a bug that made this not work properly