New Post: ADTs in TLA+

Using Abstract Data Types in TLA+. It’s an adaptation of part of my TLAConf talk. It’s also a lot more advanced than most of the material I put online, and I expect it to only be useful to experienced TLA+ users. But that stuff is important, too. The community has made a lot of improvements in beginner-level instruction, so now there’s more of an audience for advanced techniques. I want those people to keep learning, too.

I don’t really have a formalized theory of the impact of “skill ceilings”, but I want to think they’re bad. In particular I’m pretty jealous of the Haskell community, which is really good at forever raising the skill ceiling. You can argue they don’t give enough priority to beginners and intermediates, and I think that’s a fair critique, but I also believe they do a much better job of pushing the boundaries of their world than other language commuities do. And I want that in formal methods, too.

See also: Blub Studies.

Uncomfortable Truths in Software Engineering

Between the Alloy 6 drop, a workshop, and some personal stuff, I’ve been really frazzled mentally. I’m hoping to have the mental capacity to go back to full newsletters next week, but for now, I want to do something a little lighter on me.1 So here are some uncomfortable truths I believe about software engineering!

To be clear, these are uncomfortable truths to me. You might think they’re all great things! And I believe them, but I’m not committed to them. I haven’t deeply researched all of these, you might be able to convince me otherwise, things could change about the culture, etc. I didn’t bother to sort these or make sure they’re not redundant. So here we go:

1. Most people don’t care about the things I care about, for any possible definition of “things”, “care”, and “I”.
   • But especially so with me, given I care about weird exotic technology at the boundary of programming.
2. Sophisticated DSLs with special syntax are probably a dead-end. Ruby and Scala both leaned hard into this and neither got it to catch on.
3. Absent other factors, statically-typed languages are better for large projects than dynamically-typed languages. There’s no rigorous academic evidence for this, but a lot of companies have been backporting typescript/mypy/sorbet onto existing dynamic codebases and the case studies have been overwhelmingly positive. While dynamic languages can be the right choice for a large project, you have to make the case for why it’s the right choice, like a killer library, something particular to the domain, etc.
4. Empirical research on software engineering is a trainwreck and will remain a trainwreck for the forseeable future.
5. Formal methods will never be mainstream, nor will property-based testing, nor will any correctness technique that requires a large amount of training to be effective, no matter how effective it actually is.
   • Software projects are highly vulnerable to entropy. Any technique or process that requires continuous upkeep is going to decay, unless the C-suite commits to maintaining it.
6. We don’t have the Alan Kay / Free Software / Hypercard dream of everybody having control over their own computer because integrating with disparate APIs is really fucking hard and takes a lot of work to do. This will never get better, because API design is decentralized and everybody is going to make different decisions with their APIs.
   • Also, “trivial knowledge” blocks most projects from happening. To work with any new API or domain, you have to learn a lot of stuff that is “trivial” to an experienced user of that API, but you have to repeat the learning process for every single thing you want to add in, which doesn’t scale.
   • Also also, making software customizable / interfaceable is really hard on the developers for little benefit, since most people won’t use it anyway, so there’s better use of their resources.
   • Also also also, most muggles don’t want to program their own computers, much in the same way that most muggles don’t want to do their own taxes or wire their own houses.
7. Despite my personal reservations, pairing is probably better than two solo devs if both pairers can handle it. Mobbing is probably better than pairing.
   • I should probably write why I think this, but that’s a whole essay in itself. Basically it comes back to “trivial knowledge” being a blocker, which is elided with mobbing.
8. Teams predominantly care about intra-team friction in their practices. They will prefer tools and techniques that everybody already knows over things that only one person knows and everybody else has to learn. This means that new ideas have to fight much, much harder to be adopted by teams than by individuals.
   • Teams will never broadly adopt Sphinx/rST or Sphinx/MyST, because everybody already knows how to use markdown.
   • Did I mention formal methods will never be mainstream?
9. The Unix philosophy of “do one thing well” doesn’t actually work that well. Dan Luu explains this better than I could.
10. TDD/FP/Agile zealots are probably zealots because adopting TDD/FP/Agile/Whatever made them better programmers than they were before. If the choice is between them being zealots and them not learning the new techniques, it’s probably better for their company and their development that they’re zealots.
    • I mean it would be better if they learned TDD/FP/Agile/Whatever without becoming zealots, and incorporated their ideas into an overall synthesis of a nuanced programming philosophy, but I don’t think most people are interested in doing that anyway.
    • Possibly because “synthesizing a nuanced programming philosophy” only matters / is useful to a very small slice of programmers, because it’s honestly a kinda weird thing to expect tens of millions of people to be that weirdly obsessive about their job.
11. Any technical interview is going to be gameable and exclusionary to some underrepresented group/background. It’s very possible that our current dysfunctional interviewing practices are still, somehow, close to optimal.
12. The open source maintainer problem isn’t going to get much better in the near future.
    • People are gonna keep blaming “Capitalism” for this.
    • People are gonna keep blaming “Capitalism” for a lot of irrelevant things.
    • People are gonna argue with me about blaming “Capitalism”.
    • Goddamn I am so tired of “the problem is CAPITALISM” takes and they will never stop
13. We’re never going to get the broader SE culture to care about things like performance, compatibility, accessibility, security, or privacy, at least not without legal regulations that are enforced.
    • And regulations are written in blood, so we’ll only get enforced legal regulations after a lack of accessibility kills people.

A lot of these are really cynical, but they’re about the overall software engineering world, which consists of hundreds of thousands of companies and tens of millions of developers. We can still make things locally better, and that’s enough for me to keep trying.