Merchants on the Ivory Road
Before we get into the main bit I have a few announcements to cover:
Announcements
New essay
I wrote a new essay! The Frink is Good, the Unit is Evil. Learn why units of measure are so annoying to work with and why a lot of languages just give up and shunt them off to a library.
Fun fact: this is the first article I spent money on! I commissioned someone to make the header image. Zardoz!
Office hours
Been a while, hasn't it?
Office hours will be 11 AM Friday CST, (4 PM UTC).
Zoom room is 872 6064 7536
, password is
679272
, link is here. Feel free to ask anything you like about formal methods, software history, really anything I do.
I'm going to be spending this week working on my TLA+ workshop so that'll probably be the main thing on my mind. But questions on anything are totally appreciated!
PLTalk Appearance this Friday
Speaking of Friday, at 5 PM CST I will be on PLTalk! I'll be talking formal methods with Jean Yang and Hongyi Hu. One's a programming language theorist (PLT) and the other is a security engineer, so expect the discussion to get spicy.
Toxx Clause
If I don't complete the first draft of the Crossover Project essay by the end of September, I will give 1,000 USD to a random newsletter subscriber.1
Merchants on the Ivory Road
This is been on my mind for a while. But it's really become a dominant thought because of a few things happening in rapid succession:
- Greg Wilson, a longtime inspiration of mine, just won the ACM Influential Educator Award. In his acceptance speech, he notes that he's developed a lot of ways to better teach software, but none of them have effectively gone mainstream.
- I'm helping a mathematician friend transition to programming. One of the smartest guys I ever met. He likes to make jokes about how useless the math he did was. Then we'll be pairing on an exercise and he'll say something like "hmmm this reminds me of [obscure 2016 paper on Noetherian modules]" and come back the next day with a 100x optimization. It's impressive and just a little bit terrifying.
- Jean Yang started a newsletter where she compares PLT to high fashion. She argues that a lot of work in PLT eventually "trickles down" to mainstream. The examples she gives are garbage collection and abstract data types.
- In email correspondence with someone, they called me "Dr". They'd assumed that I had a PhD in computer science. In reality, I just have bachelors in physics and math, both of which I've totally forgotten. I took all of two CS in college, one on functional programming and one on automata theory.2
Phenomenology
Here's one of the few things I do remember about physics. In most of physics, there are two kinds of researchers: theorists and experimentalists. Theorists are the people who come up with math models to explain the world. Experimentalists actually test those models. Of course it's a bit complicated than that but the core idea is there. Theorists try to explain the experiments, experimentalists try to validate the theories.
High-energy physics is different. High-energy physics is the stuff layfolk think of as "cutting edge". Particle accelerators. CERN. The Large Hadron Collider. In high-energy physics, the experimental tools can take the work of thousands of people to design and build. It is experimentalism pushed to the extremes, where science blurs into engineering. The sheer difficulty in running experiments means that the theory has become a field unto itself.3 The theory and experiment are so specialized that the overlap between them, already tenuous in other fields of physics, disappears completely.
So in high-energy physics there exists a third kind of physicist: the phenomenologist. The phenomenologist takes the theorists' theories and comes up with predictions for experiments. They take the experimentalists' data and interpret what it means for the theories. They are the intermediaries that make both worlds function.
The phenomenologists exist because of the gulf between having an idea and applying the idea. Being able to take fundamental research and turn it into something applicable is itself a difficult skill.
The Ivory Road
I think there's a similar thing between software research and the software industry. There are a lot of really great ideas in academia that never reach the industry. Many academics blame this on industry "not caring" about quality or something. Many industry people blame this on academics being out of touch, not knowing what industry really needs.
But both sides to this are wrong. A lot of academia could be very useful to industry, and industry wants to adopt useful ideas from academia. It even goes both ways: there are many important developments in industry that academics don't research. The issue is both simpler and more complicated: moving ideas between the two worlds is hard. It's like there's a long and treacherous ivory road, barely travelled, the essential difficulty heightened even more by how few people try to cross it.
I'm not an academic, but I'm not quite an industry person either. I think I'm a good programmer but not a great one. I believe that many of the newsletter subscribers are better than me, often much better. My skills are in trying to dig through obscure work in computer science and finding things that can be applied more broadly. Often the reasons these aren't applied is a mixture of poor education and poor marketing. That's what I can "import". I can make things more exciting and accessible to people.
Greg Wilson and Jean Yang are the same, although they have more academic credentials and technical proficiency than I do. I'm excited about my mathematician friend for the same reasons. He can bring mathematics to everyday life. Compared to that, making mathematics useful for software engineers is a cakewalk.
(Another major person: Andreas Zeller. He was the first person to make tests shrinking useful outside academia, as he talks about in his ICSE lecture. He's currently working to mainstream fuzzing.)
Formal methods is something I'm successfully importing. I don't mean that I am the sole person who popularized it. There are many merchants on the ivory road. But I still helped! I made software engineering better not through inventing or programming, but through learning, writing, and curating. In a sense, it's "ideas guy" made useful. This is where I feel most comfortable being, the mix of history, journalism, writing, programming.
It feels kind of weird in some ways, too, like I'm not a "real" programmer because I don't spend nearly as much time programming as real programmers do. And I worry about losing connection. If I'm not programming, I don't have the same lived experience as people who do, so all of my research and writing might be completely out-of-touch with practitioners. Like the gurus who had a good idea 40 years ago and devolve into a cult of personality. That is a dangerous path.
On the other hand, I think we fill a much-needed role in the broader software ecosystem. A role much-needed in part because people don't realize it's missing. I don't know how the other people I've listed feel about this topic. Do they think the same way? Do they find being called an importer versus how they defined themselves to be demeaning? I don't know.
What I do know is that this concept hasn't really been talked about… well, anywhere. So it's worth calling attention to it. If we want industry and academia to collaborate more, we need to travel the ivory road.
-
If there are any issues transferring the money, I will instead donate the money to a charity of that subscriber's choice. ↩
-
To this day I am irrationally evangelical about SML. ↩
-
The flip side of this is astrophysics, where we can easily detect things like dark matter and oh-my-god particles but have no idea how to explain them. The joke is that particle physics is theory without data and astro is data without theory. ↩
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.