launch ftw, part 8
Brian Hicks, July 4, 2023
After asking around, it turns out that people "in" the formal methods community aren't really that numerous and don't seem to hang out a lot online, or they hang out in tool-specific places. I get the feeling, though, that that's just where the experts hang out… what about the beginners? People struggling to get their heads around what they want to do? Where can they be found? Same question about people looking to hire or buy services—is that LinkedIn? Somewhere else?
I feel like I'm asking the same questions I was asking when looking for Sorbet chat, but with more of a sense that something is out there for me to find. I've seen people mentioning formal methods online far more than I've seen them mentioning Sorbet, so those folks are surely out there, right?
Some things I've looked at to try and verify that I'm not in a bubble again:
- search on Lobsters for "formal methods." There's some discussion, but as you'd expect it's mostly around the links that people submit.
- searched for "formal methods" on LinkedIn for the same. Got a few job ads and some spammy results. I know there's discussion there, but I suspect you have to be connected to the right people (and I'm not, at least on that platform.) Searching
#formalverification gets a few better results, but it's not a lot of discussion. - searched for "formal methods" on Hacker News. Lots of people using the term in different and incompatible ways, which implies that they are probably outside the space or are using it colloquially (which seems common for Hacker News.)
- searched for "formal methods" on one of the watering holes I found in Ruby-land. There are people actually talking about this! Interesting! Mostly, though, they're repeating the claim that Ruby is impossible to analyze because of how dynamic/metaprogrammy it is. Common refrain.
This isn't a lot to go on, but I haven't looked at Reddit or tool-specific forums like Dafny, Alloy, etc yet. I am now remembering how many LaTeX-formatted papers you need to go through to make progress in this space, though, which indicates that there is a lot of academic work. I'm not in those spaces, though, and I suspect I'd struggle to break in.
That's all the time I have for today, so we'll have to pick this up next time.