bytes.zone

launch ftw, part 9

Brian Hicks, July 5, 2023

I'm currently in a "business hack and chat" meeting with some Recurse Center alumni! I'm gonna spend 45 minutes looking for people chatting about improving with formal methods (instead of just using the term colloquially or publishing papers about their use.) My hit list: look around on subreddits, then look in some tool-specific forums to see if there are newbies there. I'm thinking Alloy and TLA+ to start, but maybe I'll find more around the edges.

(2 minutes in) OK, let's try /r/formalmethods first. That seems broad. … Well, maybe overbroad. There appear to be only about 20 posts in the last year, and quite a few of them seem to be promotion-focused instead of asking questions. Some learning posts show up, though: someone is interested in pursuing a PhD in formal methods, someone who is having trouble with a graduate program, someone asking for review of an Alloy model (but they're asking to ask, so there are no actual replies in the last year), someone trying to find practitioners to interview, someone who has made a "pragmatic guide to formal modeling", and someone wondering how to make FM more popular. Most of these seem like OK threads to try and read to get a sense of people's struggles, but overall it doesn't seem like this is a place I could get involved in community—it's just too slow!

(10 minutes in) However, there was a link to /r/systems_engineering that seems much larger and some of the posts use "formal" in a way that seems promising. But once I looked at it, it seems like this is a large-scale traditional engineering thing. Lots of ™s and ®s after the official pages of these products. There's definitely money there waiting to be spent, but it's not something that I have any particular skill or advantage in.

(15 minutes in) Looked at /r/tlaplus briefly. It wasn't super promising. Seems low-traffic again. Reddit asked me if the subreddit had profanity in its name. I said "no" and then it asked me if there's profanity in the posts. I mean, I don't know man… I don't not swear when I'm using TLA+, great though it is.

(26 minutes in) It's probably about time to go look at tool-specific forums. I know about the Alloy discourse, which is helpful but fairly slow-paced. I snagged some threads to read later there, though. There's also a TLA+ Google Group. (Side note: TLA+ is probably the best-known formal methods tool in my circles, so I'd probably end up using a lot of it… is that where I want to take this business? I'm not sure I do!)

OK, 30 minutes in. Time for some OODA:

  1. Observe: what am I feeling, why, and what is my impulse?
    • What am I feeling? I'm feeling discouraged and a little stressed.
    • Why? Discouraged because I can't find the kinds of things I'm looking for, stressed because OH NO this is the second time what if I can't EVER FIND ANYTHING???? Drama drama drama drama. (Only feeling this a little, fortunately.)
    • What is my impulse? Call this another "no" and switch audiences again.
  2. Orient:
    • What is happening?
      • I spent 45 minutes or so finding not very much in the common locations, although I didn't look extensively on StackOverflow.
      • The folks I emailed say there's no big mass of FM folks hanging out online (except on LinkedIn, where folks have landed after Twitter.)
    • What does the data say? The kind of discussion I want to read and participate in doesn't exist, at least not in places that are accessible for me.
    • What do I want? I want a place to get a slightly easier foothold.
  3. Decide: Sounds like it's time to broaden my search in one of a couple ways:
    • I could go back to Ruby, but focus on Ruby for itself now instead of Ruby for Sorbet's sake.
    • I could do the next item on my possibilities list, which is something in frontend. Maybe CSS?
    • I could try and come up with more possibilities and analyze those.
  4. Act: At the risk of overanalysis, I think I'm going to try and brainstorm a few more possibilities tomorrow.