Sup Nerds, We Doin' a Mailbag

First some good personal news: I did a hiatus over the summer due to severe depression issues. Well, I finally got into an intensive outpatient program, which so far seems to be helping, and I'm optimistic it'll leave me in a better place longterm.

Now some bad professional news: IOPs are both really time-consuming and mentally exhausting, which makes it hard to do more than my core client work. Don't get me wrong, I want to write and I have the capacity to write, but there's also a ton of research, synthesis, and editing that goes into the usual blogposts and newsletters. That's why the last newsletter was pretty off-the-cuff opinions— it's a lot less mental overhead.

So this week I'll do another low-stress thing and provide short answers to several topics. Specifically, these topics:

Note that all my answers are gonna be short and mostly I know off the top of my head, without research or going deep into nuance. Each of these could be their own 2000-word essay.

First words are links to the individual tweets.

Static type systems — are they formal methods?

Depends on the system. It's true that all static type systems prove some formal properties of your program, but formal methods as a discipline is concerned with the tools and skills required to prove arbitrary properties. And that requires a very different approach.

My rough rule of thumb is that a formal verification coding language should be able to, at the very least, write a provably-correct leftpad. Lots of languages have type systems powerful enough for this, such as Idris, Liquid Haskell, and Agda. So a sufficiently-strong type system counts as formal methods, but those end up being much more complex than "production" type systems.

(Oh uh if this is your first time hearing "formal methods", you might find this post helpful. And this one, which is also way shorter. I write a lot about formal methods.)

Would be interested in your thoughts on [the Swiss Cheese Model]

The Swiss Cheese Model is a mental model of system safety. Tests catch some bugs, code review catches other bugs, linting more. Each also has holes, but the bugs missed by tests are likely to be caught by code review, and the bugs missed by those two are caught by linting, etc. So even though a bug might pass through one hole in a "slice of swiss cheese", it will hit eventually hit the cheese in a different layer and be stopped.

It's a more specific version of Defense in Depth, which I talked about a bit here. DiD is generally a good thing; the problem is the SCM tends to portray the layers as indepedent, when often the layers gradually couple to each other. Resource limitations and social priorities align the holes, so some defects can bypass everything.

Also, systemic issues support each other. The bug doesn't fly in a straight line. Nancy Leveson talks about this a bit here.

year end retrospective on "are we really engineers"

Gonna about this as part of my general end-of-year retrospective (probably next week), but overall disappointed with how little of a splash it made. I was hoping it would start more public discussion about software engineering, but it was just like any other popular post: frontpaged a few sites, lots of grandstanding by people who clearly didn't read the article, and then everyone moved on. I still get emails occasionally, which is nice, but it feels little anticlimactic for the two years of work I put into it.

I also submitted it to a couple of conferences but wasn't accepted. I'm gonna try again in 2022 but I was certain it was a dead-ringer for a conf talk and now I'm not expecting it to get anywhere.

I should be clear I'm disappointed, not bitter. It's ultimately the nature of creating public content, things just work that way.

(Man, now I want to start pushing it again. It's still some of the best work I've ever done, IMO.)

The most bizarre/ridiculous failures that you can imagine and haven’t seen yet, but expect to see in the future

I'm honestly surprised we haven't seen more failures caused by implanted state agents. Not like "cyberhackers exploiting a bug in Twitter to hack accounts", but "ASIS agent joins AWS as a software engineering, gradually rises in the ranks, then deletes the entire New Zealand government cloud." Obvs nothing that dramatic is going to happen, but there's so much information in these companies and they're always hiring so many engineers, right? There's gotta be a few people exfiltrating source code, at the very least.

I guess that's not too ridiculous, so some more bizarre stuff:

• Using MMORPG clients as nodes in a massive DDOS
• The dreaded reverse-leap second
• An instance of ML data poisoning in the wild
• AWS is forced to permanently shut down an entire region
• Google depreciates search
• Failure caused by meteor strike

the answer is always j

So f^:_ runs f until the result stops changing:

   NB. 2&0. is cos
   2&o. 0
1
   2&o. 1p0
0.540302

   NB. fixpoint of cos(x)
   2&o.^:_ ] 1p0
0.739085

Turns out that f^:a: does the same thing, but also accumulates all the intermediate values!

  2&o.^:a: ] 1.5p0
1.5 0.0707372 0.997499 0.542405 0.85647 0.655109 \
0.792982 0.701724 0.76373 0.722261 0.750313 \
0.731476 0.74419 0.735637 ...

Seems mostly useful when doing horrible things with agendas and gerunds and stuff, and also for impressing your friends.

(I'm sort of drafting a piece on "Recreational J" and part of scoring solutions is "how many weird features of J you can use instead of escape hatches")

The 7 people you meet at a conference (and how to write about them for SEO purposes)

God I've wanted to do something like this for a while, where the piece looks like it's gonna be a joke listicle and then it suddenly jukes into really specific and useful categories, like

1. The first timer who's being sent by their company, and they're really nervous and think they need to get their money's worth by going to as many talks as possible
2. The person who's there to hang out with friends they only get to hang out with at conferences
3. The group sent by their company so the company can showcase how cool and tech-focused they are, and they may or may not be loyal enough to do that vs enjoy the conference
4. The person who's there on a diversity scholarship and is worried others won't take them seriously or think they're less competent, even though the scholar knows diversity scholarships don't work like that
5. People trying to navigate the conference with other commitments, like kids, a family illness, or being on-call
6. Speakers who wouldn't have attended the conference if they weren't speakers, but now that they're here they plan to enjoy it anyway
7. People who aren't really that into the topics of the conference but like tech people and the conference is local to their city so might as well check it out

Obvs people can belong to more than one category, and also if I made an actual piece about that I'd spend more than 5 minutes thinking of categories. I'm surprised as it is I was able to come up with seven on the spot

Formal Methods and DBs? Like do Query Optimizers and stuff use Formal Methods under the hood in any way?

As a rule of thumb, the answer to "does technology domain $x use formal methods" is "no". There's going to be individual technologies that use it, but you're unlikely to see widespread use.

I know a lot of database companies— Elastic, Cockroach, Mongo, Azure, AWS— are using formal methods for parts of their databases, but I don't know if any of this work is with the query optimizer. But this could just be a limitation on my end: I'm not too familiar with database technology or how query optimizers work. I wouldn't be surprised if at least one notable company is experimenting with it, but I wouldn't be surprised if nobody had any verified optimizer parts, either.

Okay that's all I have time for today, this was fun and I should do this more often, unless people manage to find gaping factual errors in all of these answers, in which case I should never do it again

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.