New Post: Formally Modeling Database Migrations
Hi everybody,
I wrote a new post for the blog! It's about how you can use formal methods to make sure your database migrations are correct. I really wanted to do a post like this for a couple big reasons:
- Alloy reminds me of SQL, so I figured "hey, might as well write a DB-oriented example"
- One of the current limitations of FM is that we only really have examples for two domains: really low level stuff and distributed systems. And that makes sense, because they're really useful for that! But it makes people think that FM is only useful for those two domains.
I think there are two approaches to discovering FM. The first is to do think "wow, this would be really useful for distributed systems! I should check this out if I ever have to do a DS." And that's totally reasonable. When I first discovered FM, though, I had a different thought: "This is something I thought was impossible. The domain is distributed systems, but it's still something impossible. What else can we do? What else is out there‽"
Of course, I don't expect everybody to have the same reaction I do. Which is why it's important for me, as a teacher and advocate, to expand the space that people see is possible. Make it easy for people to realize that FM is not just for distributed systems, but many other things, too. The field is small, not for a lack of functionality, but for a lack of people who are exploring its limits. The more people I can get using it, the more we'll discover is possible.
If you're curious about more "exotic uses" of formal methods, here are a couple of fun ones. They're all scientific papers, so not the easiest things to read, but still!
- Some people experimenting with using Petri nets to model business workflows: here. I'm in general skeptical of the wider benefits of Petri nets, but they're fun and it's an interesting domain to apply them to.
- Using Alloy to model scientific simulations: here. I really like this paper and need to write a full summary so people don't have to grind through it themselves.
...I really thought I had more than two links, but most of the rest aren't close to as exotic as those two. Welp, that's an excuse to do more digging!
H
PS: Still need a name. If nobody has any good ideas I might just go with "Programming Stuff"
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.