Workshop Innovations and New Website Essay

Office hours

What I'm thinking of doing is office hours every two weeks, alternating between an evening slot and a morning slot. So this week let's do office hours at 8 PM CST Thursday, 1 AM UTC. Room is [redacted], password is [redacted], link is [redacted]. Feel free to ask any questions you have about formal methods, software history, anything I specialize in.

New essay: constructive versus predicative data

It's out! I shared a first draft with you all earlier, but the polished version is now available here. Feel free to share this one around :-)

(I feel really weird having released four articles in a row that are less than 2000 words. They're still pretty long the absolute standards, but given the two articles before those were about 6000 and 4000 words each… Change in priorities, I guess.)

Workshop innovations

So as most of you know, my big push for the next couple weeks is improving my Alloy workshop. And there's a lot of work to do with that. Not only have I already given it before, I've already given it online before, so the amount of work I have to do is might seem surprising. Normally you would expect that once you've written a workshop you're done. All future work is on maintenance, small tweaks, corrections, stuff like that. The problem is that every time I run the workshop, I get new ideas of how to make it radically better. Here's some stuff I want to add to this one:

Messy examples

For TLA+ the best examples are what I call "simple, innocent, obvious, wrong". Specs that are short and obviously correct, except that they aren't. But I've struggled with finding similar examples for Alloy. The problem is that the easiest way to make something SIOW is to introduce concurrency which has all sorts of subtle and nasty nonsense. Concurrency is a beginner topic in TLA+ and an advanced topic in Alloy. Alloy is much better at describing the relationships between static things than the behavior of dynamic things.

I was testing a new examples last week when I realized that I was approaching this wrong. The goal of SIOW is to show people that they can't just reason through these things informally, they need to use a proper tool. But maybe instead of showing how their intuition is wrong, I could instead give the models that intuitively seem too complicated to reason about. Instead of avoiding the mess, lean into the mess. Present nasty business domains with lots of quirky rules and show how alloy can generate satisfying examples for you to explore in more detail.

I whipped up a quick example of Spotify playlists in alloy and had it generate some visualizations. Here's one it spat out:¹

Look at how beautiful that is! If you were trying to informally reason through your system properties, would you want to have to test an example like this? Would you even think of an example like this? Not only can Alloy test this model for your properties, it can test all possible models of this size in a fraction of a second. If I can capture that excitement with messy models, it would do a lot to sell the value of alloy to the workshop attendees.

Incremental labs

My classes are divided into group exercises, individual exercises, and labs. The purpose of labs is to study an existing spec and understand how it works better. I usually start by going through it line by line, going around and asking each person to explain that line. My problem is that this is time-consuming enough that I can't really afford to have people write the specs themselves. So I provided to them already. The specs come in multiple "stages" for different sections of the lab. As you move the next stage, they copy and paste the new version.

// part 1
A
B


// part 2
A'
B
C

This means they spend less time actually writing the syntax of a spec. While this is much less important in understanding the essence of specification, getting used to putting all of the keywords in the right places reduces the pain down the line. This then gets reserved for the individual drills. If I can move some of this practice to the labs it means more time for teaching essentials versus practicing syntax.

To get more "typing" practice in, I want to instead provide a diff of the new stage from the old one, as opposed to the new stage as a whole. It would look kind of like this:

// part 1
A
B

// part 2
- A
+ A'
B
+ C

Now they can still quickly get to the new stage, but also get some practice comparing the changes and typing things out manually. It's a small change, but every 2% improvement to the workshop's efficiency corresponds to an extra ten minutes of teaching time. Those kinds of savings add up.

(I will also provide the new stage as a side thing in case you will fall behind or get out of sync. But it will be the fallback, not the default.)

Discussion questions

I'm not sure where I'm going to go with this but I really like the idea. Most of the questions I have are to test their understanding of alloy. I looked at more questions that test their understanding of the philosophy of specification. I think it would look more like active discussions between the people in the class, where they have to talk about the relative trade-offs between a set of different but valid approaches. I'll sleep on this one.

Not all of these improvements will happen in the June 8 workshop due to time constraints. Lots of smaller tweaks and updates to exercises take priority. But I eventually want to incorporate all these improvements as well as the progressive cheat sheets I talked about a while back. I really gotta write an article on that...

That's all from me. Have a great week!

H

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.