Full Width [alt+shift+f] Shortcuts [alt+shift+k]
Sign Up [alt+shift+s] Log In [alt+shift+l]

Computer Things

Computer Things
How to convince engineers that formal methods is cool Sorry there was no newsletter last week! I got COVID. Still got it, which is why this one's also...
4 months ago
60
4 months ago
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...
Computer Things
Refactoring Invariants (Feeling a little sick so this one will be short.) I'm often asked by clients to review their...
5 months ago
59
5 months ago
(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...
Computer Things
Hyperproperties I wrote about hyperproperties on my blog four years ago, but now an intriguing client problem got me...
3 months ago
58
3 months ago
I wrote about hyperproperties on my blog four years ago, but now an intriguing client problem got me thinking about them again.1 We're using TLA+ to model a system that starts in state A, and under certain complicated conditions P, transitions to state B. They also had a flag f...
Computer Things
Why Not Comments Logic For Programmers v0.3 Now available! It's a light release as I learn more about formatting a...
5 months ago
55
5 months ago
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...
Computer Things
Formally modeling dreidel, the sequel Channukah's next week and that means my favorite pastime, complaining about how Dreidel is a bad...
2 months ago
55
2 months ago
Channukah's next week and that means my favorite pastime, complaining about how Dreidel is a bad game. Last year I formally modeled it in PRISM to prove the game's not fun. But because I limited the model to only a small case, I couldn't prove the game was truly bad. It's time...
Computer Things
What could be added to TLA+ Last week Leslie Lamport posted The Future of TLA+, saying "the future of TLA+ is in the hands of...
5 months ago
54
5 months ago
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...
Computer Things
Be Suspicious of Success From Leslie Lamport's Specifying Systems: You should be suspicious if [the model checker] does not...
4 months ago
53
4 months ago
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...
Computer Things
TLA from first principles No Newsletter next week I'll be speaking at USENIX SRECon! TLA from first principles I'm working on...
4 months ago
52
4 months ago
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....
Computer Things
"Logic for Programmers" Project Update Happy new year everyone! I released the first Logic for Programmers alpha six months ago. There's...
a month ago
49
a month ago
Happy new year everyone! I released the first Logic for Programmers alpha six months ago. There's since been four new versions since then, with the November release putting us in beta. Between work and holidays I didn't make much progress in December, but there will be a 0.6...
Computer Things
Goodhart's Law in Software Engineering Blog Hiatus You might have noticed I haven't been updating my website. I haven't even looked at any...
5 months ago
49
5 months ago
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....
Computer Things
Stroustrop's Rule Just finished two weeks of workshops and am exhausted, so this one will be light. Hanuka Sale Logic...
2 months ago
47
2 months ago
Just finished two weeks of workshops and am exhausted, so this one will be light. Hanuka Sale Logic for Programmers is on sale until the end of Chanukah! That's Jan 2nd if you're not Jewish. Get it for 40% off here. Stroustrop's Rule I first encountered Stroustrop's Rule on this...
Computer Things
A list of ternary operators Sup nerds, I'm back from SREcon! I had a blast, despite knowing nothing about site reliability...
3 months ago
47
3 months ago
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...
Computer Things
Five Unusual Raku Features Logic for Programmers is now in Beta! v0.5 marks the official end of alpha! With the new version,...
3 months ago
44
3 months ago
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...
Computer Things
State and time are the same thing Time is state Imagine I put an ordinary ticking quartz clock in an empty room. I walk in, and ten...
5 months ago
44
5 months ago
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...
Computer Things
An idea for teaching formal methods better I was recently commissioned by a company to make a bespoke TLA+ workshop with a strong emphasis on...
6 months ago
36
6 months ago
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...
Computer Things
What are the Rosettas of formal specification? First of all, I just released version 0.6 of Logic for Programmers! You can get it here. Release...
a month ago
36
a month ago
First of all, I just released version 0.6 of Logic for Programmers! You can get it here. Release notes in the footnote.1 I've been thinking about my next project after the book's done. One idea is to do a survey of new formal specification languages. There's been a lot of new...
Computer Things
Stroustrup's Rule Just finished two weeks of workshops and am exhausted, so this one will be light. Hanuka Sale Logic...
2 months ago
36
2 months ago
Just finished two weeks of workshops and am exhausted, so this one will be light. Hanuka Sale Logic for Programmers is on sale until the end of Chanukah! That's Jan 2nd if you're not Jewish. Get it for 40% off here. Stroustrup's Rule I first encountered Stroustrup's Rule on this...
Computer Things
The Juggler's Curse I'm making a more focused effort to juggle this year. Mostly boxes, but also classic balls too.1...
a month ago
34
a month ago
I'm making a more focused effort to juggle this year. Mostly boxes, but also classic balls too.1 I've gotten to the point where I can almost consistently do a five-ball cascade, which I thought was the cutoff to being a "good juggler". "Thought" because I now know a "good...
Computer Things
Texttools dot py I make a lot of personal software tools. One of these is "texttools.py", which is easiest to explain...
6 months ago
29
6 months ago
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...
Computer Things
Why I prefer rST to markdown I just published a new version of Logic for Programmers! v0.2 has epub support, content on...
6 months ago
25
6 months ago
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...
Computer Things
My patented Miracle Tonic would have prevented the CrowdStrike meltdown Last Friday CrowdStrike did something really bad and it destroyed every airport in the world. I...
7 months ago
24
7 months ago
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...
Computer Things
A brief introduction to interval arithmetic You've got a wall in your apartment and a couch. You measure the wall with a ruler and get 7 feet,...
8 months ago
23
8 months ago
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...
Computer Things
Solving a math problem with planner programming The deadline for the logic book is coming up! I'm hoping to have it ready for early access by either...
7 months ago
22
7 months ago
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,...
Computer Things
Keep perfecting your config First of all, I wanted to extend a huge and heartfelt thank you to all of the people who bought...
7 months ago
21
7 months ago
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...
Computer Things
Nondeterminism in Formal Specification Just an unordered collections of thoughts on this. In programming languages, nondeterminism tends to...
8 months ago
19
8 months ago
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...
Computer Things
Logic for Programmers now in early access! I am delighted to announce that Logic for Programmers is now available for purchase! While still in...
7 months ago
18
7 months ago
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...
Computer Things
What hard thing does your tech make easy? I occasionally receive emails asking me to look at the writer's new language/library/tool. Sometimes...
3 weeks ago
18
3 weeks ago
I occasionally receive emails asking me to look at the writer's new language/library/tool. Sometimes it's in an area I know well, like formal methods. Other times, I'm a complete stranger to the field. Regardless, I'm generally happy to check it out. When starting out, this is...
Computer Things
What does 'TLA+' mean, anyway TLA+ Workshop Feb 12th. I've decided to reduce the class size from 20 to 15, so there's only a...
a year ago
18
a year ago
TLA+ Workshop Feb 12th. I've decided to reduce the class size from 20 to 15, so there's only a couple of slots left! I'll be making a little less money this way but it should lead to a better teaching experience for the attendees. Use the code NEWSLETTERDISCOUNT for $100...
Computer Things
Logic for Programmers Update I spent the early week recovering and the later week working on Logic for Programmers ([init]...
8 months ago
17
8 months ago
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...
Computer Things
New blog post: Composing TLA+ Specifications Post here! It's a really advanced TLA+ technique that I'm sure will alienate 90% of my readers....
8 months ago
17
8 months ago
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.
Computer Things
I've been thinking about tradeoffs all wrong Sup nerds, I'm back from DDD Europe! Still processing the conference and adjusting to the horrible...
8 months ago
16
8 months ago
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...
Computer Things
Strings do too many things No Newsletter next week TLA+ Workshop and moving places. Strings do too many things In the unusual...
a year ago
15
a year ago
No Newsletter next week TLA+ Workshop and moving places. Strings do too many things In the unusual basis types email1 I wrote this about strings: We use strings for identifiers, human writing, structured data, and grammars. If you instead use symbols for identifiers then you can...
Computer Things
How to argue for something without any scientific evidence Last week I got this interesting question: I want to write a book about automated testing. Much of...
11 months ago
14
11 months ago
Last week I got this interesting question: I want to write a book about automated testing. Much of the book would be me explaining the best practices I’ve learned. I know these are good practices; I’ve seen them work over and over again. But have no [scientific] data at all to...
Computer Things
"Testing can show the presence of bugs but not the absence" Program testing can be used to show the presence of bugs, but never to show their absence! — Edgar...
10 months ago
14
10 months ago
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...
Computer Things
Some notes on for loops New Blogpost Don't let Alloy facts make your specs a fiction, about formal methods practices (and a...
10 months ago
13
10 months ago
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...
Computer Things
What makes concurrency so hard? A lot of my formal specification projects involve concurrent or distributed system. That's in the...
10 months ago
13
10 months ago
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...
Computer Things
Unusual basis types in programming languages TLA+ Workshop TLA+ workshop on Feb 12! Learn how to find complex bugs in software systems before you...
a year ago
13
a year ago
TLA+ Workshop TLA+ workshop on Feb 12! Learn how to find complex bugs in software systems before you start building them. I've been saying the code NEWSLETTERDISCOUNT gives $50 off, but that's wrong because I actually set it up for $100 off. Enjoy! Unusual basis types in...
Computer Things
What I look for in empirical software papers Behind on the talk and still reading a lot of research papers on empirical software engineering...
9 months ago
13
9 months ago
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...
Computer Things
GitHub Search for research and learning Hi everyone! I have a new blog post out: An RNG that runs in your brain. It's a mix of cool tricks...
a year ago
13
a year ago
Hi everyone! I have a new blog post out: An RNG that runs in your brain. It's a mix of cool tricks and math analysis done with an exotic gremlin language. Patreon is here. Also TLA+ workshop on Feb 12 etc etc use the code NEWSLETTERDISCOUNT for $100 off etc Anyway I've been all...
Computer Things
Planning vs Model Checking New blogpost! Planner programming blows my mind, Patreon here. Next essay out should be the graph...
a year ago
13
a year ago
New blogpost! Planner programming blows my mind, Patreon here. Next essay out should be the graph project. The post is about Picat and more specifically, planner programming. Planning very roughly is: You provide a start state, a set of goals, and a set of state transitions...
Computer Things
What if the spec doesn't match the code? Whenever I talk about formal methods, I get the same question: Can I use the spec to generate my...
11 months ago
13
11 months ago
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...
Computer Things
What Mob Programming is Bad At Pairing is two people working together to write code, while mobbing is three or more. Pairing has...
11 months ago
12
11 months ago
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...
Computer Things
"Integration tests" are just vibes New blog post! Software Friction is about how all the small issues we run into developing software...
9 months ago
12
9 months ago
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...
Computer Things
NoCode Will Not Bring Computing to the Masses No Newsletter next week I'll be giving my conference talk at DDD Europe. NoCode Will Not Bring...
9 months ago
12
9 months ago
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...
Computer Things
Why do regexes use `$` and `^` as line anchors? Next week is April Cools! A bunch of tech bloggers will be writing about a bunch of non-tech topics....
11 months ago
12
11 months ago
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...
Computer Things
Paradigms succeed when you can strip them for parts I'm speaking at DDD Europe about Empirical Software Engineering!1 I have complicated thoughts about...
9 months ago
11
9 months ago
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...
Computer Things
Are Efficiency and Horizontal Scalability at odds? Sorry for missing the newsletter last week! I started writing on Monday as normal, and by Wednesday...
a week ago
11
a week ago
Sorry for missing the newsletter last week! I started writing on Monday as normal, and by Wednesday the piece (about the hierarchy of controls ) was 2000 words and not close to done. So now it'll be a blog post sometime later this month. I also just released a new version of...
Computer Things
Know (of) the right tool for the job Last week's Picat essay did pretty well online! One of the common responses was "This looks really...
12 months ago
11
12 months ago
Last week's Picat essay did pretty well online! One of the common responses was "This looks really interesting but I don't know where I'd use it." For Picat there was a gap of five years between me hearing about it and actually learning it. The same is true for most of the weird...
Computer Things
What makes concurrency so hard? A lot of my formal specification projects involve concurrent or distributed system. That's in the...
10 months ago
10
10 months ago
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...
Computer Things
Five Kinds of Nondeterminism No newsletter next week, I'm teaching a TLA+ workshop. Speaking of which: I spend a lot of time...
3 days ago
7
3 days ago
No newsletter next week, I'm teaching a TLA+ workshop. Speaking of which: I spend a lot of time thinking about formal methods (and TLA+ specifically) because it's where the source of almost all my revenue. But I don't share most of the details because 90% of my readers don't use...