Let's make the CPython team regret adding pattern matching to Python! | Continue reading
Back in 2007 Python added Abstract Base Classes, which were intended to be used as interfaces:from abc import ABC class AbstractIterable(ABC): @abstractmethod def __iter__(self): while False: yield None def get_iterator(self): return self.__iter__() ABCs were added to strengthen … | Continue reading
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 … | Continue reading
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 Pract … | Continue reading
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 … | Continue reading
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 a … | Continue reading
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 langua … | Continue reading
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 writi … | Continue reading
I sat in front of Mat, idly chatting about tech and cuisine. Before now, I had known him mostly for his cooking pictures on Twitter, the kind that made me envious of suburbanites and their 75,000 BTU woks. But now he was the test subject for my new project, to see if it was going … | Continue reading
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+.1Imagine we’re designing a multithreaded counter. We don’t know how we’re going to implement it y … | Continue reading
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 inpu … | Continue reading
“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 Devicesend(to, from, count) register short *to, *from; register count; { register n = (count + 7) / 8; switch (count % 8) { case 0: do { *t … | Continue reading
“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 Devicesend(to, from, count) register short *to, *from; register count; { register n = (count + 7) / 8; switch (count % 8) { case 0: do { *t … | Continue reading
This is the companion reference for A Brief Introduction to Esoteric Languages, my lecture for a friend’s college class. The video should be legible to other viewers, and the material here should be (mostly) understandable without watching the video. The Esolangs Listed roughly … | Continue reading
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 … | Continue reading
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 … | Continue reading
In 2010 Carmen Reinhart and Kenneth Rogoff published Growth in a Time of Debt. It’s arguably one of the most influential economics papers of the decade, convincing the IMF to push austerity measures in the European debt crisis. It was a very, very big deal.In 2013 they shared the … | Continue reading
This is part three of the crossover project. Part 1 is here and part 2 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 memori … | Continue reading
I sat in front of Mat, idly chatting about tech and cuisine. Before now, I had known him mostly for his cooking pictures on Twitter, the kind that made me envious of suburbanites and their 75,000 BTU woks. But now he was the test subject for my new project, to see if it was going … | Continue reading
I sat in front of Mat, idly chatting about tech and cuisine. Before now, I had known him mostly for his cooking pictures on Twitter, the kind that made me envious of suburbanites and their 75,000 BTU woks. But now he was the test subject for my new project, to see if it was going … | Continue reading
Last month I researched two historical questions. I originally posted summaries on Twitter and am reproducing both here.1Why 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 Ex … | Continue reading
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 s … | Continue reading
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 s … | Continue reading
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 abou … | Continue reading
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 th … | Continue reading
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 noth … | Continue reading
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, proba … | Continue reading
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: ce … | Continue reading
This post has been translated into Russian by Timur Kadirov. Thank you!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 arbit … | Continue reading
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 t … | Continue reading
Consider a data type that represents users, which includes “favorite people” and “blocked people”:1data 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 c … | Continue reading
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 re … | Continue reading
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 nee … | Continue reading
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 everythin … | Continue reading
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”. Preposte … | Continue reading
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”. Preposte … | Continue reading
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 “a … | Continue reading
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 doe … | Continue reading
This post has been translated into Russian by Timur Kadirov. Thank you!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 arbit … | Continue reading
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 isolat … | Continue reading
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 mate … | Continue reading
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? … | Continue reading
When we design programs, we usually look for two kinds of properties: that “bad things” never happen and that “good things” always happen. These are called safety and liveness properties, respectively. These are properties that we want to hold true for every possible program beha … | Continue reading
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. … | Continue reading
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 us … | Continue reading
Back in 2007 Python added Abstract Base Classes, which were intended to be used as interfaces:from abc import ABC class AbstractIterable(ABC): @abstractmethod def __iter__(self): while False: yield None def get_iterator(self): return self.__iter__() ABCs were added to strengthen … | Continue reading
Official Description: You’ve used pytest and you’ve used mypy, but bugs are still slipping through your code. What’s next? In this talk, we cover two simple but powerful tools for keeping your code problem-free. Property-based testing, provided by the Hypothesis library, lets you … | Continue reading