All of my budgeted blogwriting time is going to Logic for Programmers. Should be back early 2025. (I’m still writing the weekly newsletter.)
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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...
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....
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")...
I haven’t written much about TLA+ on the blog since the new learntla went up. Any examples or special topics I think of go there instead. But I recently thought of a cool demo that doesn’t quite fit the theme of that book: there are some things you can’t easily check with the model checker but can check if you work with the state space as a...
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...
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...
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 =...
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...
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...
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...
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...
img {border-style: groove; border-width: 1px; padding: 5px; } Sounds like I should write a post on safety and liveness! First, some definitions. A system is anything that has changing state. This is an incredibly broad definition that covers a wide variety of situations, like: Two threads in a thread scheduler Five servers behind a load...
Mimicry is when software X reimplements at a higher level a core feature of software Y. The produced facsimile has some, but not all, of the same properties, enough to “look like” it’s the same thing but missing many of the nuances. This exists in every kind of software. One language can mimic another, a library can mimic a language, a database...
One of my favorite little bits of python is __subclasshook__. Abstract Base Classes with __subclasshook__ can define what counts as a subclass of the ABC, even if the target doesn’t know about the ABC. For example: class PalindromicName(ABC): @classmethod def __subclasshook__(cls, C): name = C.__name__.lower() return name[::-1] == name class...
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...
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...
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...
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...
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....
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...
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...
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...
“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++;...
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 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...
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...
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...
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...
This is part one of the Crossover Project. Part two is here and part three is here. 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...
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...
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...
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...
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...
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...
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...
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:...
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....
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....
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...
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...
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...
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...
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...
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”...
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...
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...
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...
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...
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...
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...
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 the duck typing a little. If you inherited AbstractIterable, then...
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...
Many bugs are implementation errors: there is a mistake in the code that makes it not do what you wanted it to do. For example, you may have accidentally left out the “list is empty” case, or written a nonterminating function. You can identify it as “definitely wrong” for a given input. Most testing, in fact most writing on software correctness,...
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...
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...
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...
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...
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]:
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...
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...
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...
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...
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...
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...
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...
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...
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,...
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...
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...
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...
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...
Good UI is necessary to making correct software. If people have trouble using the product, they’re more likely to do the wrong thing. Personally, though, I can’t stand UI work. I don’t think it’s “beneath me” or anything, it just doesn’t quite mesh with my brain. Visuals and interfaces give me anxiety. Mad respect for the people who can handle...
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...
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...
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....
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...
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...
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...
“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 ⇔...
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...
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...
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...
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...
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...
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...
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...
One of my vices is watching Link to the Past Randomizer games. This gist is it’s a regular Zelda game except all of the items in chests are randomized. A chest that normally has bombs might have a critical item, while the chest that’s supposed to have the moon pearl might only have 10 rupees. People use randomizers to run races, since you can’t...
I want to call attention to one of the best papers I’ve ever read on software engineering, ever. Ready to be dazzled? Here goes: Fixing Faults in C and Java Source Code: Abbreviated vs. Full-Word Identifier Names (preprint) I know, right? Sheer brilliance. Okay, maybe it doesn’t have the most exciting subject matter, but I think everybody should...
Vim has one of the best macro systems of any text editor out there. Here’s why: Macros are just stored keystrokes. When you record a macro, it’s saved to the appropriate register, and it can be pasted and appended like any other saved string. When you run the macro, Vim simulates you typing every single character in the register. There are a...
I’m a pretty big fan of contracts and property-based testing. While they’re both powerful, they do have tradeoffs: Contracts are simple and allow for complex conditionals, but you need to test them over a wide space to confirm them. Property-Based Testing can test your code over a very wide search space, but you have to come up with good...
“Use the right tool for the job” is a pretty tired cliche. Mostly it’s used to dismiss overengineering and one-size-fits-all solutions to problems, like using microservices for your 10-user app. It isn’t a bad saying, it’s just tautologically true. I don’t think anybody wants to use the wrong tool for the job, unless they’re trying to sabotage...
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...
At work we’re discussing moving some stuff to microservices. A lot of people said that they like “how microservices separate concerns while monoliths entangle them”. Others argued that “monoliths can be separated just fine with modules”, to which someone responded “it’s really hard to keep modules separate”. But “don’t you have the same problem...
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...
In January I start EMT Training and maybe make at least one of my childhood dreams come true. I’ve been saving for years for this: while the program is cheap, I’m effectively losing my monthly salary. I found it really easy to calculate my burn rate in J. I’ve talked about J before so I’ll assume you know the basics and we can skip all of that....
After my recent vitriol about unit testing, a couple of people sent me Why TDD is Crap as a thorough debunking of TDD and unit testing. As someone very interested in software correctness, I ended up writing a debunking of his debunking. Transcriptions will be in quotes, my responses below. Some important notes: From what can tell, neither of us...
This is an absolutely insane idea and I’m delighted by its audacity so I’m sharing it with all y’all. There’s like a bazillion things wrong with it but saying dumb shit has never stopped me before so let’s do some grambling! The way I see it, unit tests act as a frame around your coding. The most common practice is you write the tests to cover...
I think by hand. It’s easier for me to write my first drafts on a tablet and type them up afterwards. I can’t do this with code, though. Here’s me scrawling out a python function as fast as possible: That took three times longer to write than type. Something about code being optimized for legibility and IDE usage and lame stuff like that. I still...
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...
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; },...
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 their code with another team, who quickly found a bug. Once corrected,...
This post is about the Hypothesis testing library. If you’re unfamiliar with it, check it out! Property tests are a fantastic addition to your testing suite. All examples use pytest. Imagine we’ve written a bubblesort: def bubblesort(l: List[int]) -> List[int]: # blah blah blah What are some of the properties we could test? We could check that...
There are a lot of curated lists out there about good programming resources. One thing they all have in common is that they’re focused on relatively mainstream ideas: good languages, good techniques, etc. I want to try something a little different and focus on the articles that are skeptical about what everybody believes in programming. To keep...
I’m working on some examples for my TLA+ guide and realized this one would be a good introduction to specification in general, so I simplified it a little to make it more accessible. Enjoy! The problem Deploying code to a set of servers is tricky. You can turn them off, migrate the code, and turn them back on, but that’ll piss off the customers....
I’m working on some examples for my TLA+ guide and realized this one would be a good introduction to specification in general, so I simplified it a little to make it more accessible. Enjoy! The problem Deploying code to a set of servers is tricky. You can turn them off, migrate the code, and turn them back on, but that’ll piss off the customers....
Doctests are one of the most fascinating things in Python. Not necessarily because it’s particularly elegant or useful, but because it’s unique: I haven’t found another language that has a similar kind of feature. Here’s how it works. Imagine I was writing an adder: def add(a,b): return a + b There’s two kinds of ways we can test it. The first...
Let’s start with a couple of premises: There are 10x programmers out there, Some programming techniques are better than others. I don’t think either of these is particularly controversial. The first is pretty widely accepted and borne out by studies. And we see examples of the second everywhere: see for example all of the pissfights about...