TLA+ Helped Me Count to Six
The TLA+ Workshop is done! I'm taking November off from workshops do complete three writing goals:
- Feedback from the first draft of the Crossover Project is in, so time to get a second draft done.
- Have enough of Predicate Logic for Programmers written that I can put it up as a book-in-progress on Leanpub and not feel like I'm conning people.
- Write errata for Practical TLA+. I promised to do that in October and then, uh, didn't. November it is!
Next Alloy workshop will be early December and next TLA+ workshop will be January.
TLA+ Helped Me Count to Six
I end my workshops by taking student-provided systems and writing specs for them as a group. When I first started doing this, I noticed something interesting: even though it'd be an unfamiliar domain, I'd discover design errors much faster than the student. This is really great for teaching: "Okay, so you just added a retry mechanism. Before you run the model, try to identify the race condition." That kind of thing.
Using TLA+ has changed how I see designs, how my brain works. Race conditions and deadlocks become a visceral thing, a wrongness in the system that I feel physically. I have enough experience analyzing specifications that I start processing them on an intuitive level. Two takeaways from this:
- Learning formal methods can help you design better. I mean duh, I staked my career on this.
- Your brain can normalize unnatural things.
That's not as crazy as it sounds. What's 4×7? Did you get 28? Did you get it by adding four sevens together? Or did you memorize the multiplication table?
The multiplication table is something that you have to train yourself to use well, but once you do, it makes it a lot easier to do something. We learn a lot of these things in elementary school but stop after that for some reason. The only adult-equivalent I can think of is memory palaces. It's easier to memorize things if you fix them in a geographic space, like your apartment or childhood home. This takes practice but is really effective once you get the hang of it. I practiced with Codenames cards and at one point had 40 of them memorized.
Which brings me to counting. How many squares are in this picture?
How fast did you get four? Did you count four or did you see four? Okay, let's try this again. How many squares?
How fast did you get 12? Did you count 12 or did you see 12? There's a point where you can't just see the number anymore, you have to count them. For me, the threshold is five. I can see five things but need to count six. And because I'm a huge weirdo I'm often in situations where I want to count things quickly. Can I train myself to see higher?
The term for this is subitizing, which is the worst-sounding word I learned all year. Subitization is the process of exactly determining the number of objects in a collection without having to explicitly count them. I looked for resources on improving my subitization but all the resources are for teaching children. Children can barely subitize two, and then gradually get better until they can subitize around four, where it stabilizes. If I want to improve my adult subitization then I'm on my own.
Not everything in our minds is trainable. I've done some research on working memory, where we can only keep a few things in short-term memory at once, and the consensus seems to be that humans can't change that number. But other things we can train. I trained to instantly know that 6×7 is 42, to use memory palaces, and to see design flaws in TLA+ specs. Not to mention there's a precedent for subitizing larger numbers at a glance:
Even if you don't see nine, you saw the nine there, because of the 3x3 shape. Maybe I can tap into the geometric intuition to build out my seeing. I wrote a program to help me practice. Nothing complicated, just put 4-9 squares at random on the screen so that I can count them. I hope that if I practice for 5-10 minutes a day I'll eventually be able to subitize more than five squares at a time. Here's the whole program:
What, you don't recognize that? It's a language called Drape. Released in 1998, Drape is a programming environment for kids. I used it because it makes drawing easy and I didn't want to learn any actual graphics libraries. Also because it was the first programming language I ever learned. I was 10 at the time and had no idea what I was getting into. I was surprised that I still had a copy of the program in storage somewhere and enjoyed using it again.
I started practicing with this a couple days back and plan to do a few minutes each day. I think I'm getting better at seeing six but won't know for certain for a while.
If you're interested in trying Drape you can download it here. The license is free to distribute for noncommercial purposes. Warning, it only works in Windows and has a fixed resolution. I would be surprised if it didn't work on WINE, though.
Knacks
This isn't the first time I've tried to learn a weird mental skill. I call them "knacks" for some reason. Not complete mental disciplines, not party tricks, just small things that come often. I've been fascinated with them ever since I learned about compass belts. Some I've tried to learn to varying degrees of success:
- Memory palaces.
- Precisely counting out ten seconds in my head. I got it down to about a 5% error until I stopped practicing and it drifted back to
- Divides tables. What's 5/7th of a cup of flour?
- "Caching" and "uncaching" thoughts as a way to help with ADD.
- Getting an intuitive sense of what metric measurements mean, in the same way I have it for US customary units, without having to convert.
- How to read flag semaphore for some inexplicable reason.
Some of these are obviously more useful than others. What knacks have you learned, and what would you recommend learning?
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.