Before we get into the main bit I have a few announcements to cover:
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!
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!
872 6064 7536
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.
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
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:
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.
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. ↩