Blog on Hillel Wayne

For latency, anyway.

My work brings me though a lot of software correctness techniques, things like type theory, test-driven development (TDD), and formal methods.

My job these days is teaching TLA+ and formal methods: specifying designs to find bugs in them.

Decision tables are easy, simple, and powerful.

Kenneth Iverson’s 1964 language, APL, won him the Turing Award.

Now that teach workshops for a living, I spend a lot of time on making better workshops.

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.

I’m in the process of revising some of my workshops.

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.

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

People think it’s weird that I do all my development on a Windows machine.

I want to do $THING.

tl;dr: online Alloy reference here.

The other day I read 20 most significant programming languages in history, a “preposterous table I just made up.”

I love science.

In most testing frameworks, you’re expected to write a lot of low-level tests and few high-level tests.

This is an “intro packet” you can use to argue for the benefits of formal methods (FM) to your boss.

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.

I speak very fast.

Most of my formal methods examples deal with concurrency, because time is evil and I hate it.

Back in 2007 Python added Abstract Base Classes, which were intended to be used as interfaces: fromabc import ABC classAbstractIterable(ABC): @abstractmethod def__iter__(self): while False: yield None defget_iterator(self): return self.

Last year I got certified as an EMT.

Many bugs are implementation errors: there is a mistake in the code that makes it not do what you wanted it to do.

In my job I dig up a lot of obscure techniques.

I’ve been using Vim for eight years and am still discovering new things.

People keep claiming that modern OOP languages aren’t “really OOP” because they don’t follow Alan Kay’s definition of “OOP”.

A common question I get about specs is how to model bad actors.

A while back I was ranting about APLs and included this python code to get the mode of a list: defmode(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

Confession: I read the ACM Magazine.

A few people have told me that they’ve enjoyed learning formal methods but aren’t sure how to actually use it.

There’s a famous logic puzzle, originally from Raymond Smullyan, called a “Knights and Knaves” puzzle.

I saw this question on the Software Engineering Stack Exchange: What are the barriers that prevent widespread adoption of formal methods?

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 investig…

Caveats: I’m not an interviewer, I’ve never done serious research on interviews, and I haven’t tested this.

I recently did a corporate TLA+ workshop and some people asked what TLA+ specs look like in practice.

Update 2024-08-28: I’ve since released a free online book, Learn TLA+, that supersedes Practical TLA+.

This is part two of a two-part article.

This is part one of a two-part article.

Disclaimer 2024-12-02 Since this rant is going viral again (again (again)), some disclaimers: I wrote this six years ago to “”“win”“” an ugly Twitter fight.

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.

I really like decision tables but they’ve fallen out of common knowledge.

Good UI is necessary to making correct software.

This is an excerpt from Michael Jackson (not the singer)’s book Software Requirements and Specifications, in his discussion of “Raw Materials”.

Functional programming and immutability are hot right now.

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?

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.

This post was commissioned by Graham Christensen as part of the Great Slate fundraiser.

People always tell me that the hardest part of learning TLA+ is finding good examples.

“Mathematics doesn’t have a sense of time, but often we need to track time.

Note: I’m coming from this from the perspective of a J programmer.