Breaking the limits of TLA+ model checking
Graphing TLA+ state spaces for fun and profit.| Hillel Wayne
It’s April Cools! It’s like April Fools, except instead of cringe comedy you make genuine content that’s different from what you usually do. For example, last year I talked about the 3400-year history of the name “Daniel”. This year I wrote about one of my hobbies in hopes it would take less time. It didn’t. The video game industry is the biggest entertainment industry in the world. In 2024, it produced almost half a trillion dollars in revenue, compared to the film industry’s ...| Hillel Wayne
What does this print? x =1 x -->0 Think it through, then try it in a browser console! Answer and explanation in the dropdown. Show answer It prints 1. wait wtf At the beginning of a line (and only at the beginning of a line), --> starts a comment. The JavaScript is parsed as x=1; x; // 0 The browser then displays the value of the last expression, which of course is 1.| Hillel Wayne
The other day a mechanical engineer introduced me to the Hierarchy of Controls (HoC), an important concept in workplace safety. 1 (source) To protect people from hazards, system designers should seek to use the most effective controls available. This means elimination over substitution, substitution over engineering controls, etc. Can we use the Hierarchy of Controls in software engineering? Software environments are different than physical environments, but maybe there are some ideas worth e...| Hillel Wayne
All of my budgeted blogwriting time is going to Logic for Programmers. Should be back early 2025. (I’m still writing the weekly newsletter.)| Blog on Hillel Wayne
A toolbox language is a programming language that’s good at solving problems without requiring third party packages. My default toolbox languages are Python and shell scripts, which you probably already know about. Here are some of my more obscure ones. AutoHotKey Had to show up! Autohotkey is basically “shell scripting for GUIs”. Just a fantastic tool to smooth over using unprogrammable applications. It’s Windows-only but similar things exist for Mac and Linux.| Hillel Wayne
Update 01/07/19 Greetings from 2019! The good news is that Chicago isn’t yet a radioactive crater. The bad news is almost everything I said about refinement in this article is wrong. I’m working on writing a more in-depth, rigorous treatment of refinement as its own article. But this one is currently explaining something that definitely isn’t refinement. mkay thanks! Update 2020-10-05: I’m probably not going to write that article on refinement in the near future and also Chicago is a ...| Hillel Wayne
Last year a client asked me to solve a problem: they wanted to be able to compose two large TLA+ specs as part of a larger system. Normally you’re not supposed to do this and instead write one large spec with both systems hardcoded in, but these specs were enormous and had many internal invariants of their own. They needed a way to develop the two specs independently and then integrate them with minimal overhead.| Hillel Wayne
In his book On War, Clausewitz defines friction as the difference between military theory and reality: Thus, then, in strategy everything is very simple, but not on that account very easy. Everything is very simple in war, but the simplest thing is difficult. These difficulties accumulate and produce a friction, which no man can imagine exactly who has not seen war. As an instance of [friction], take the weather.| Hillel Wayne
I’ve recently done a lot of work in Alloy and it’s got me thinking about a common specification pitfall. Everything in the main post applies to all formal specifications, everything in dropdowns is for experienced Alloy users. Consider a simple model of a dependency tree. We have a set of top-level dependencies for our program, which have their own dependencies, etc. We can model it this way in Alloy:| Hillel Wayne
It’s April Cools! It’s like April Fools, except instead of cringe comedy you make genuine content that’s different what you usually do. For example, last year I talked about the strangest markets on the internet. This year I went down a different rabbit hole. Daniel has been a top 5 baby name twice since 2000. There are over 1.5 million Daniels in the United States (and almost 100,000 last-name Danielses).| Hillel Wayne
A (directed) graph is a set of nodes, connected by arrows (edges). The nodes and edges may contain data. Here are some graphs: All graphs made with graphviz (source) Graphs are ubiquitous in software engineering: Package dependencies form directed graphs, as do module imports. The internet is a graph of links between webpages. Model checkers analyze software by exploring the “state space” of all possible configurations.| Hillel Wayne
Picat is a research language intended to combine logic programming, imperative programming, and constraint solving. I originally learned it to help with vacation scheduling but soon discovered its planner module, which is one of the most fascinating programming models I’ve ever seen. First, a brief explanation of logic programming (LP). In imperative and functional programming, we take inputs and write algorithms that produce outputs. In LP and constraint solving, we instead provide a set o...| Hillel Wayne
Humans are notoriously bad at coming up with random numbers. I wanted to be able to quickly generate “random enough” numbers. I’m not looking for anything that great, I just want to be able to come up with the random digits in half a minute. Some looking around brought me to an old usenet post by George Marsaglia: Choose a 2-digit number, say 23, your “seed”. Form a new 2-digit number: the 10’s digit plus 6 times the units digit.| Hillel Wayne
This is just a way of thinking about formal specification that I find really useful. The terms originally come from Michael Jackson’s Software Requirements and Specifications. In specification, the machine is the part of the system you have direct control over and the world is all the parts that you don’t. Take a simple transfer spec: ---- MODULE transfer ---- EXTENDS TLC, Integers CONSTANTS People, Money, NumTransfers (* --algorithm transfer variables acct \in [People -> Money]; define \...| Hillel Wayne
This is my writeup of all the talks I saw at Strangeloop, written on the train ride back, while the talks were still fresh in my mind. Now that all the talks are online I can share it. This should have gone up like a month ago but I was busy and then sick. Enjoy! How to build a meaningful career Topic: How to define what “success” means to you in your career and then be successful.| Hillel Wayne
Short version: If X inherits from Y, then X should pass all of Y’s black box tests. I first encountered this idea at SPLASH 2021. The longer explanation A bit of background In A Behavioral Notion of Subtyping Liskov originally defined subtyping in inherited objects as follows: Subtype Requirement: Let P(x) be a property provable about objects x of type T. Then P(y) should be true for objects y of type S where S is a subtype of T.| Hillel Wayne
tl;dr annotated AHK scripts here. Anybody who’s spent time with me knows how much I love AutoHotKey, the flat-out best Windows automation tool in the world. Anybody’s who’s tried to use AutoHotKey knows how intimidating it can be. So to help with that, I’m sharing (almost) all of my scripts along with extensive explanations. There’s fourteen files in total, covering (among other things): Fast open specific folders on your computer Fast insertion of the current date, em-dashes, and ...| Hillel Wayne
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.) UPDATE: Currently 12,000 words into the learntla rewrite. If I don’t have something I’m happy enough to share by the end of June, I’ll give $1,000 to a random newsletter subscriber (or the charity of their choice).| Hillel Wayne
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 neve...| Hillel Wayne
tl;dr: online Alloy reference here. If you’ve read this blog at all you probably know I’m a big fan of Alloy. It’s a simple, powerful formal method whose entire syntax fits in just two pages. You can learn it in a day and be productive in two. And it can be used to model everything from package management to database migrations to authorization systems. Two years ago I was invited to the Workshop on the Future of Alloy.| Hillel Wayne
This is an excerpt from Michael Jackson (not the singer)’s book Software Requirements and Specifications, in his discussion of “Raw Materials”. It’s worth letting stand on its own. First, make a list of all the languages you use in all your development activities. Be honest: don’t list all of the languages you have ever heard of; include only languages you have used for real work at least once… Now, ask yourself which of the languages on your list you would choose to say these thi...| Hillel Wayne
Two universal facts about user documentation: Documentation is really important. We are really bad at writing it. We don’t have good theories on what makes for useful documentation. That is except for the four document model, or Diátaxis.1 I’m glad that people use it. I’m also a little frustrated that people use it even when its inappropriate. My problem is that it’s not a universal or comprehensive model: there’s a lot of documentation people need to write that doesn’t neatly fi...| Hillel Wayne
I originally ran this on my newsletter last year but I like it way too much to let it rot in the archives. Enjoy! Happy Pi Day!1 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.| Hillel Wayne
img {border-style: groove; border-width: 1px;} I love Autohotkey so much that it keeps me on Windows. It’s the best GUI automation tool out there. Here’s a shortcut that opens my current browser tab in the Wayback Machine: #HotIf WinActive("ahk_exe firefox.exe") >!^s:: { Keywait("RControl") Keywait("RAlt") SendEvent("^l") SendInput("{left}https://web.archive.org/web/*/{enter}") } #HotIf By comparison, the official extension takes four files to do the same thing. Four files!1 But I come he...| Hillel Wayne
Graphing TLA+ state spaces for fun and profit.| Hillel Wayne
It’s April Cools! It’s like April Fools, except instead of cringe comedy you make genuine content that’s different from your normal stuff.1 For example, last year I talked about owning a microscope. This year I debated doing another hobby but settled on a much dumber topic. Have you ever seen those lists of weird things you can buy online? It’s always just novelties and gag gifts. I’m much more interested in the weird things with a legitimate use case.| Hillel Wayne
I like how easy it is to configure neovim. Last month I wanted a task runner for a very particular use-case that none of the available plugins handled. So I wrote my own. Show Code This is not good code. vim.g.global_task = {} function LoadTask(cmd, num, silent) local tmp = vim.g.global_task -- (a) if not num then num = vim.tbl_count(vim.g.global_task) + 1 end tmp[tonumber(num)] = cmd -- (a) vim.| Hillel Wayne
A common assumption I see on the ‘net is that NP-complete problems are impossible to solve. I recently read that dependency management in Python is hard because package resolution is NP-complete. This is true in principle, but the reality is more complicated. When we say “NP-complete is hard” we’re talking about worst-case complexity, and the average-case complexity is often much more tractable. Many industry problems are “well-behaved” and modern SAT solvers can solve them quickly.| Hillel Wayne
Complexity is bad. Simple software is better than complex software. But software is complex for a reason. While people like coming up with grand theories of complexity (Simple Made Easy, No Silver Bullet) there’s very little info out there on the nitty-gritty specific sources of complexity. Without that, all the theories feel to me like the four elements theory. We just don’t have the data needed to come up with something more predictive.| Hillel Wayne
img {border-style: groove;} Someone recently told me a project isn’t real until you do a retrospective, so I think it’s time to do one for Let’s Prove Leftpad. Short explanation: it’s a repository of proofs of leftpad, in different proof systems. Long explanation: the rest of this post. Background I’m into formal methods, the discipline of proving software correct. Consider the following contrived code: def add(x: int, y: int): int { if(x == 12976 && y == 14867) { return x - y; } re...| Hillel Wayne
This is my writeup of all the talks I saw at Strangeloop, written on the train ride back, while the talks were still fresh in my mind. Now that all the talks are online I can share it! Next year’s the last Strange Loop. You can buy tickets here. Opening Keynote: How expert programmers think about errors Topic: What we empirically know about how experts write code. Ultimately found a lot of it pretty conventional.| Hillel Wayne
Some useful mental models from the world of formal methods.| Hillel Wayne
Sometimes software pretends to be other software.| Hillel Wayne
Let's make the CPython team regret adding pattern matching to Python!| Hillel Wayne
A while back I wrote that Robert Martin was ruining software by being too good at programming. That was supposed to be a joke. Since then he’s done his damndest to actually ruin software by telling people they’re doing it wrong. His most recent response where he yells at software correctness was the breaking point for me, so I’m going to go ahead and say what many of us have been thinking:| Hillel Wayne
A while back I was ranting about APLs and included this python code to get the mode of a list: def mode(l): max = None count = {} for x in l: if x not in count: count[x] = 0 count[x] += 1 if not max or count[x] > count[max]: max = x return max There’s a bug in it. Do you see it? If not, try running it on the list [0, 0, 1]:| Hillel Wayne
This is part two of a two-part article. Part one is here. Last time we left off with this model: include "globals.mzn"; enum DAYS; enum ROOMS; enum TIMES; enum talks; constraint assert(card(DAYS) * card(ROOMS) * card(TIMES) == card(talks), "Number of slots must match number of talks"); enum people; array[people, talks] of 0..4: pref; array[DAYS, TIMES, ROOMS] of var talks: sched; constraint alldifferent (d in DAYS, t in TIMES, r in ROOMS) (sched[d, t, r]); array[people] of var int: score; con...| Hillel Wayne
This is part one of a two-part article. Part two is here. A while back somebody told me to check out MiniZinc. Eventually I did and really enjoyed it, so figured I’d write about it here. This is actually going to be a two part article. Right now we’re talking about what it is and how it works, and in the next post we’ll talk about optimizing models. MiniZinc is a constraint solving language designed for modeling optimization problems.| Hillel Wayne
Take the following code: a = 1 a = a + 1 print(a) A common FP critique of imperative programming goes like this: “How can a = a + 1? That’s like saying 1 = 2. Mutable assignment makes no sense.” This is a notation mismatch: “equals” should mean “equality”, when it really means “assign”. I agree with this criticism and think it’s bad notation. But I also know some languages don’t write a = a + 1, instead writing a := a + 1.| Hillel Wayne
I’ve been working on a bunch of longform obligation pieces and while they’re a lot of fun, they’re also steadily driving me insane. So I took a day off to write about all of the kinds of automated testing I know about. I’m defining tests here to be “an independent verification program that, as part of verification, executes the code we want to verify.” This means types are not tests, as they don’t involve execution of the code, and contracts are not tests, because they’re not ...| Hillel Wayne
People always tell me that the hardest part of learning TLA+ is finding good examples. This makes sense to me: most of the main ones out there are either toy problems or immensely complex algorithms. It’s sort of the nature of TLA+: if you’re using it, you’re trying to design something complicated, and that’s usually because you’re trying to sell something complicated. Also, the community is tiny. You could probably fit all of the TLA+ experts in the world in a small coffee shop.| Hillel Wayne
“Mathematics doesn’t have a sense of time, but often we need to track time. So programmers borrow an idea from the field of formal logic and replace all functions (f: A → B) ↦ f: A × T → B where T is the partially ordered set t1 ... tn. If T is totally ordered we can then define a mutation as a tuple in M ⊆ Var × Val × Val × T such that ∈ M ⇔ x[b, t'] ∈ x'[a, t].| Hillel Wayne
Note: I’m coming from this from the perspective of a J programmer. Maybe K or Dyalog or something solved this already, I don’t know, but I would be pretty surprised if they did. The more I work with an APL, the more I notice a serious problem. Not the weird symbols, you get used to that pretty fast. Not the write-only aspect, that’s annoying but can be solved with a good syntax highlighter.| Hillel Wayne
In programming arguments, such as static vs dynamic typing,1 people use their experiences and reason to frame these debates. However, reason is often a poor grounding for justifying complex positions. Usually warnings against using “reason” take the form of “it’s easy to be biased” or “we tend to make logical fallacies.” But this presupposes that if we were less biased we could answer the question by thinking really hard. I’d like to argue that this is actually impossible: we ...| Hillel Wayne
I’m writing a book on TLA+! It’s going to be aimed at the same audience as Learn TLA+, but dive much deeper and go much further. I’ll be showing not just how to use TLA+, but how to think about systems, write good specifications, and fix models. I’m really excited and I’m sure you’ll be, too! I’m also trying to make it much better than Learn TLA+, because People are going to be paying money for this, so I can’t just phone it in I asked my technical reviewer to be “almost-com...| Hillel Wayne
I’m tired of hearing about Grace Hopper, Margaret Hamilton, and Ada Lovelace. Can’t we think of someone else for once? I went ahead and compiled a bunch of really important women according to some fairly arbitrary rules: There’s a specific thing you can point to and say “That. That’s their contribution.” This leaves out a lot of really qualified people who made lots of general contributions, but I wanted to keep this list fixed on soundbites.| Hillel Wayne
People say “Comments should explain why, not what.” I feel like starting a flame war today so I’m going to argue that comments should explain ‘what’ too. Please don’t use this as justification to write bad code, okay? Okay. First of all, why shouldn’t comments explain ‘what’? If you need comments to explain what’s going on, it suggests your code is unclear. If I write //weight, radius, price w = 10, r = 9, p = 1 That’s not as clear as saying| Hillel Wayne
I’ve namedropped contracts enough here that I think it’s finally time to go talk about them. A lot of people conflate them with class interfaces / dynamic typing / “your unit tests are your contract”, which muddies the discussion and makes it hard to show their benefits. So I’d like to build up the idea of contracts from first principles. We’re going to work in Python, up until the point where things get crazy.| Hillel Wayne
I recently read No excuses, write unit tests, which argues Unit Tests are Good and You Should Write Them. For the most part I strongly agree with their message, which is why I feel kinda bad criticizing the essay. They provide this as “an example of simple testing”: constadd=(...numbers) => { returnnumbers.reduce((acc, val) => { returnacc+val; }, 0); }; it('should add numbers', () => { constexpected=15; constactual=add(1, 2, 3, 4, 5); expect(actual).| Hillel Wayne
In my 2021 TLAConf Talk I introduced a technique for encoding abstract data types (ADTs). For accessibility I’m reproducing it here. This post is aimed at intermediate-level TLA+ users who already understand action properties and the general concept of refinement. Say we want to add a LIFO stack to a specification. You can push to and pop from the end of this stack but you cannot change data in the middle.| Hillel Wayne
Alloy is a powerful formal specification language, but it’s historically been weak at modeling concurrency. AWS raised this as a critical issue for why they went with TLA+. Alloy writers built a lot of tricks to emulate time, but it can feel like you’re working against the language. Alloy 6 aims to change that with built-in temporal operators. Right now it’s poorly documented, and since I maintain the alloydocs, I sat down and figured it all out.| Hillel Wayne
A Sudoku Puzzle is a famous Japanese puzzle. In it you solve a 9 by 9 grid of numbers, but you don’t need to do any math to solve the sudoku puzzle! In each number you put a row and column, and also a number in each box. We will solve the Sudoku Puzzle with programming, by writing a program that solves the Sudoku Puzzle. This can be done in any programming language.| Hillel Wayne
When teaching formal methods, I often get asked how we can connect the specifications we write to the code we produce. One way we do this is with refinement. All examples are in TLA+.1 Imagine we’re designing a multithreaded counter. We don’t know how we’re going to implement it yet, so we start by specifying the abstract behavior.2 ---- MODULE abstract ---- EXTENDS Integers, Sequences VARIABLES pc, counter vars == <> \* Two threads Threads == 1.| Hillel Wayne
This was originally a newsletter post I wrote back in December, but I kept coming back to the idea and wanted to make it easier to find. I’ve made some small edits for flow. There’s a certain class of problems that’s hard to test: The output isn’t obviously inferable from the input. The code isn’t just solving a human-tractable problem really quickly, it’s doing something where we don’t know the answer without running the program.| Hillel Wayne
“Don’t write clever code.” Why not? “Because it’s hard to understand.” People who say this think of clever code such as Duff’s Device: Duff's Device send(to, from, count) registershort*to, *from; registercount; { registern =(count +7) /8; switch(count %8) { case0: do{ *to =*from++; case7: *to =*from++; case6: *to =*from++; case5: *to =*from++; case4: *to =*from++; case3: *to =*from++; case2: *to =*from++; case1: *to =*from++; } while(--n >0); } } This code is “clever” becaus...| Hillel Wayne
Recently my friend Lars Hupel and I had a discussion on why formal methods don’t compose well. You can read the conversation here. We focused mostly on composing formally-verified code. I want to talk a little more about the difficulties in composing specifications. This is half because it’s difficult for interesting reasons and half because it’s a common question from beginners. Beginners to formal specification expect specifications should be organized like programs: multiple independ...| Hillel Wayne
A couple years back I gave a talk on researching software history, using “linked list interview questions” as an example topic. Since referring people to a video is less accessible than just writing a blog post, I’ve reproduced the question here. So why do interviewers like to ask linked list questions? If you ask people, you usually get one of two answers: “It tests CS fundamentals.” “It tests reasoning through a new problem.| Hillel Wayne
There’s not a whole lot on TLA+ technique out there: all the resources are either introductions or case studies. Good for people starting out, bad for people past that. I think we need to write more intermediate-level stuff, what Ben Kuhn calls Blub studies. Here’s an attempt at that. Most TLA+ properties are invariants, properties that must be true for every state in the behavior. If we have a simple counter:| Hillel Wayne
This is part three of the crossover project. Part one is here and part two is here. I met William at Deconstruct 2019.1 We were walking back from the pre-party—too loud for my comfort level—and I took the chance to interview him. He knew about my project and wanted to share his memories of mechanical engineering. “Most of my skills transferred seamlessly. There’s one book, Sketching User Experiences, that’s aimed at software engineers.| Hillel Wayne
This is part two of the crossover project. Part one is here and part three is here. No one thinks about moving the starting or ending point of the bridge midway through construction. -Justin Cave I had to move a bridge. -Anonymous1 Carl worked as a mechanical verification engineer: he tested oil rigs to see how much they vibrated. Humans work and live on oil rigs for long stretches of time, and if they vibrate too much it can be impossible to sleep.| Hillel Wayne
Last month I researched two historical questions. I originally posted summaries on Twitter and am reproducing both here.1 Why Vim Uses hjkl Question: Why does Vim use hjkl and not the arrow keys for navigation? Common Explanation: It keeps your fingers on the home row. Historical Explanation: Bill Joy developed vi on the ADM-3A, which didn’t have dedicated arrow keys. If you look at the ADM keyboard, it put the arrow keys on the hjkl keys.| Hillel Wayne
For latency, anyway. A common architecture pattern is the “task queue”: tasks enter an ordered queue, workers pop tasks and process them. This pattern is used everywhere from distributed systems to thread pools. It applies just as well to human systems, like waiting in line at a supermarket or a bank. Task queues are popular because they are simple, easy to understand, and scale well. There are two primary performance metrics for a task queue.| Hillel Wayne
My work brings me though a lot of software correctness techniques, things like type theory, test-driven development (TDD), and formal methods. The surrounding communities all have the same problem: they can’t get people using these techniques. They all ask “Don’t people care about correct software?” To which the insiders usually answer “programmers don’t care about correctness, they just care about shoveling out garbage to make money!” I’ve heard this from every single communi...| Hillel Wayne
My job these days is teaching TLA+ and formal methods: specifying designs to find bugs in them. But just knowing the syntax isn’t enough to write specs, and it helps to have examples to draw from. I recently read Chris Siebenmann’s Even in Go, concurrency is still not easy and thought it would make a good case study for writing a spec. In it, he gives an example of Go code which deadlocks:| Hillel Wayne
Decision tables are easy, simple, and powerful. You can teach them in five minutes and write one in half that time. You can look at a table and understand what it’s saying, see if it matches your problem, and check for design flaws. So it’s kinda weird that there’s basically nothing about them online. I wrote an introduction a while back, but I want something a little more formal. So this post will reintroduce the core ideas in a more formal way and then talk about some of the technique...| Hillel Wayne
Kenneth Iverson’s 1964 language, APL, won him the Turing Award. His award lecture, Notation as a Tool of Thought, argued that better notations would lead people to deeper insights about mathematics. He provided a number of examples ranging across linear algebra, arithmetic, probability, and logic. Unfortunately, most of the mathematics he covers isn’t relevant to programming. However, his core idea still applies, and changing how we describe programs changes how we think about them.| Hillel Wayne
Now that teach workshops for a living, I spend a lot of time on making better workshops. One improvement I made was creating progressive cheatsheets. I’ll discuss the motivation and implementation below, but this is the high level picture: .gallery { display: flex; text-align: center; } .gallery a { margin: 5px; border-width: 1px; border-style: solid; } Progressions #1 and #2 of the cheatsheet. Click for full size.| Hillel Wayne
One day Alan Eliasen read a fart joke and got so mad he invented a programming language. 20 years later Frink is one of the best special purpose languages for dealing with units. “But why do we need a language just for dealing with units?” Glad you asked! Intro to Units A unit is the physical property a number represents, like distance or time. We almost always are talking about SI units, or Système international.| Hillel Wayne
I’m in the process of revising some of my workshops. I realized that one particular important aspect of TLA+, fairness, is something that I’ve struggled to explain well. Then again, everybody struggles to explain it well! It’s also a great example of how messy concurrent systems can get, so I figured it would make a good post for the blog. Stuttering Take the following spec of a clock. I used TLA+ but it should mostly be clear from context:| Hillel Wayne
This was originally written as a tutorial for Hypothesis and will eventually be reproduced there, but it might still be useful for people using other property-testing libraries. This essay assumes some familiarity with Hypothesis. If you haven’t used it, a better introduction is here. Once you learn the basics, there are two hard parts to writing property-based tests: What are good properties to test? How do I generate complex inputs?| Hillel Wayne
Consider a data type that represents users, which includes “favorite people” and “blocked people”:1 data Person: favorites: set of Person blocked: set of Person We want a validation that says that these two sets are disjoint, a.k.a. no person can belong to both sets at once. We call these kinds of validations predicates, or boolean functions that correspond to our requirements. The predicates determine if a representable item is also a valid item.| Hillel Wayne
People think it’s weird that I do all my development on a Windows machine. It’s definitely a second-class citizen experience in the wider development world, and Windows has a lot of really frustrating issues, but it’s still my favorite operating system. This is for exactly one reason: AutoHotKey. AHK is an engine for mapping keystrokes to scripts. I wouldn’t call it particularly elegant, and it’s filled with tons of redundancy and quirks.| Hillel Wayne
I want to do $THING. Normally I do my hacking in Python, which is okay but has lots of frustrations. My friends tell me $LANGUAGE is better for doing $THING. After going through the online tutorial, I can see why. Maybe I’ll try $LANGUAGE for this project! Just a few things I need to figure out first: How do I install it? The docs say brew install, but I’m on Windows.| Hillel Wayne
The other day I read 20 most significant programming languages in history, a “preposterous table I just made up.” He certainly got preposterous right: he lists Go as “most significant” but not ALGOL, Smalltalk, or ML. He also leaves off Pascal because it’s “mostly dead”. Preposterous! That defeats the whole point of what “significant in history” means. So let’s talk about some “mostly dead” languages and why they matter so much.| Hillel Wayne
I love science. Not the “space is beautiful” faux-science, but the process of doing science. Hours spent calibrating equipment, cross-checking cites of cites of cites, tedious arguments about p-values and prediction intervals, all the stuff that makes science Go. And, when it does happen, the drama. I also want us to use more empirical science in software. That’s why I wrote a talk on it! One thing lay folk don’t realize is that science is social.| Hillel Wayne
In most testing frameworks, you’re expected to write a lot of low-level tests and few high-level tests. The reasoning is that end-to-end tests are slow and expensive and only cover a tiny amount of the program’s state space. It’s better to focus on testing all the parts in isolation versus testing that they all work together. In practice, global correctness does not follow from local correctness. It’s possible for every part to be individually rock-solid but the system to be broken as...| Hillel Wayne
This is an “intro packet” you can use to argue for the benefits of formal methods (FM) to your boss. It’s a short explanation, a list of benefits and case studies, and a demo. Everything’s in TLA+, but the arguments apply equally well to Alloy, B, statecharts, etc. Adapt the material to your specific needs. Quick notational note: I’m leaving out the code verification side of formal methods, mostly because design verification is a much easier sell.| Hillel Wayne
When we design programs, we usually look for two kinds of properties: that “bad things” never happen and that “good things” are guaranteed to happen. These are called safety and liveness properties, respectively. These are properties that we want to hold true for every possible program behavior. “We always complete every request” is a liveness property. If our system has it, every program trace will complete every request. If it doesn’t hold, I can give you a example behavior wh...| Hillel Wayne
I speak very fast. It’s like the words are piled up in my mouth and I can’t say one without the rest tumbling out. Through my whole life people have told me to slow down, speak more clearly, and enunciate. I can do it if I concentrate but I quickly relapse into gushing out words. As I now give lots of conference talks, this has become a professional issue:| Hillel Wayne
Most of my formal methods examples deal with concurrency, because time is evil and I hate it. While FM is very effective for that, it gives people a limited sense of how flexible these tools are. One of the most common questions I get from people is Formal methods looks really useful for distributed systems, but I’m not making a distributed system. Is FM still useful for me?| Hillel Wayne
Last year I got certified as an EMT. As part of the training I shadowed an ambulance for a day and assisted with each run. For each patient we treated, we had to fill out a patient care report. A patient care report. (source) EMTs are just one part in a long chain. If they transport a patient to a hospital, the hospital needs to know everything about the patient and everything that happened since the call.| Hillel Wayne
In my job I dig up a lot of obscure techniques. Some of them are broadly useful: formal specification, design-by-contract, etc. These I specialize in. Some of them are useful, but for a smaller group of programmers. That’s stuff like metamorphic testing, theorem proving, constraint solving. These I write articles about. Then there’s the stuff where I have no idea how to make it useful. Either they’re so incredibly specialist or they could be useful if it weren’t for some deep problems.| Hillel Wayne
I’ve been using Vim for eight years and am still discovering new things. This is usually seen as a Good Thing About Vim. In my head, though, it’s a failing of discoverability: I keep discovering new things because Vim makes it so hard to know what’s available. While people often talk about the beauty of modal editing or text objects, I don’t think that gets at the essence of Vim.| Hillel Wayne
People keep claiming that modern OOP languages aren’t “really OOP” because they don’t follow Alan Kay’s definition of “OOP”. I can see the logic here, even if I disagree the conclusion. More recently I’ve seen people start claiming that Kay invented objects entirely. This is factually incorrect. Alan Kay did not invent objects. They come from Simula, which the Smalltalk-72 manual cites as a major inspiration (pg 117). The famous 1981 Byte magazine issue that popularized Smallt...| Hillel Wayne
A common question I get about specs is how to model bad actors. Usually this is one of two contexts: The spec involves several interacting agents sharing a protocol, but some of the nodes are faulty or malicious: they will intentionally try to subvert the system. The spec involves an agent subject to outside forces, like someone can throw a rock at your sensor. These “open world” situations are a great place to use formal methods.| Hillel Wayne
Confession: I read the ACM Magazine. This makes me a dweeb even in programming circles. One of the things I found in it is “Metamorphic Testing”. I’ve never heard of it, and nobody I knew heard about it either. But the academic literature was shockingly impressive: many incredibly successful case studies in wildly different fields. So why haven’t we heard of it before? There’s only one article anywhere targeted at people outside academia.| Hillel Wayne
A few people have told me that they’ve enjoyed learning formal methods but aren’t sure how to actually use it. They’re mostly doing short sprints at work and aren’t building new systems from scratch. This tells me there’s some confusion about what makes specifications useful, and that we need a resource on applying them in practice. This is a short guide to using specifications at work in a way that’s accessible to beginners, applicable in many contexts, and provides solid busines...| Hillel Wayne
There’s a famous logic puzzle, originally from Raymond Smullyan, called a “Knights and Knaves” puzzle. We have a set of people, all of whom are either a Knight or a Knave. Knights only make true statements, and Knaves only make false statements. Usually the goal of the puzzle is to find out who is what. For example, if we have two people, A and B, and A says “both of us are knaves”, we know A is a knave and B is a knight.| Hillel Wayne
I saw this question on the Software Engineering Stack Exchange: What are the barriers that prevent widespread adoption of formal methods? The question was closed as opinion-based, and most of the answers were things like “its too expensive!!!” or “website isn’t airplane!!!” These are sorta kinda true but don’t explain very much. I wrote this to provide a larger historical picture of formal methods, why they’re actually so unused, and what we’re doing to make them used.| Hillel Wayne
The goal of a STAMP-based analysis is to determine why the events occurred… and to identify the changes that could prevent them and similar events in the future. 1 One of my big heroes is Nancy Leveson, who did a bunch of stuff like the Therac-25 investigation and debunking N-version programming. She studies what makes software unsafe and what we can do about that. More recently she’s advocated the “STAMP model” for understanding systems.| Hillel Wayne
Caveats: I’m not an interviewer, I’ve never done serious research on interviews, and I haven’t tested this. I propose this entirely as a thought experiment. Assumptions: We interview at jobs to find ideal candidates. WE are looking for candidates who are Good at programming Good at software engineering Can work in a team A “culture fit” (not an asshole). Technical interviews test the first two. They are primarily whiteboard questions, abstract design questions, or “write this prog...| Hillel Wayne
I recently did a corporate TLA+ workshop and some people asked what TLA+ specs look like in practice. If you looked at the most common public examples, you’d probably come away thinking that people only used it for critical consensus algorithms. This is a problem for two reasons: first, it makes it harder to learn TLA+, as there aren’t simpler examples to experiment with. Second, it makes it hard for people to see how TLA+ is useful for them.| Hillel Wayne
I am delighted to announce that my book, Practical TLA+, is now available! When I stumbled into TLA+ in 2016 I had no idea it would so define my passions, my values, and my career. I definitely didn’t think I’d be writing a book. But 11 months and 220 pages later, here we are! This is the largest project I’ve ever done and I’m incredibly excited to share it with you all.| Hillel Wayne
Have a tweet: img {border-style: groove;} I have no idea if Pony is making the right choice here, I don’t know Pony, and I don’t have any interest in learning Pony.1 But this tweet raised my hackles for two reasons: It’s pretty smug. I have very strong opinions about programming, but one rule I try to follow is do not mock other programmers.2 Programming is too big and I’m too small to understand everything.| Hillel Wayne
I really like the c2 wiki as a historical artifact: a lot of big names in Agile and Extreme Programming argued with each other there.1 One thing they did was the Extreme Programming Challenge, where people tried to test the limits of these approaches. They’d find edge problems (designing databases, remote teams, etc) and see if Agile/XP still worked in that context. In almost every case they quickly decided that yes, it works just fine.| Hillel Wayne
I really like decision tables but they’ve fallen out of common knowledge. Let’s fix that. A decision table is a means of concisely representing branching and conditional computations. In the most basic form, you have some columns that represent the “inputs” as booleans and some columns that represent outputs and effects. It looks like this: A B C f(A, B, C) T T T 1 T T F 3 T F T 7 T F F “cucumber” F - - NullError - means that it doesn’t matter what the value is.| Hillel Wayne
Functional programming and immutability are hot right now. On one hand, this is pretty great as there’s lots of nice things about functional programming. On the other hand, people get a little overzealous and start claiming that imperative code is unnatural or that purity is always preferable to mutation. I think that the appropriate paradigm is heavily dependent on context, but a lot of people speak in universals. I keep hearing that it’s easier to analyze pure functional code than mutab...| Hillel Wayne
This post was commissioned by Graham Christensen as part of the Great Slate fundraiser. Thank you! I wanted to help out the Great Slate fundraiser and donated two technical essays of the purchaser’s choice. Graham bought one and asked for Something that has to do with Nix or NixOS This was a bit of a challenge, given that I didn’t even know what Nix was. I had never used it and still haven’t, nor can I use it for the near future, because my only computer right now is a Windows box.| Hillel Wayne
I recently read Tomas Petricek’s Thinking the Unthinkable, where he argues that modern PLT makes several restrictive assumptions about the nature of programming. Our reliance on mathematics in CS is not fundamental and our obsession with formal logic and algorithms keeps us from seeing other possible paradigms. He proposes two other unthinkable paradigms that are unrelatable to modern mathematical programming. I disagree with his premises: I think there’s a very valid reason to ground asp...| Hillel Wayne
To celebrate April Fools, some friends and I made content outside our normal brands. You can see the full list of pieces here! Also, CW: grody gross-up pictures of bugs. I’ve always loved science. At one time, I thought it’d be my career: I got BAs in math and physics with the hope of eventually becoming a physicist. But my friend’s horror stories of grad school scared me off and I instead left academia and got a job programming.| Hillel Wayne
