I started this blog five years ago, in January 2013. At the time, I lived in Bloomington, Indiana and was in the middle of my fifth year of grad school. I had started working on a new project with a new advisor in my fourth year — not exactly a highly recommended approach to finishing a Ph.D. — and I wanted a place to write about what I was working on. I hadn’t managed to get any papers about my project accepted yet, but they couldn’t stop me from blogging, dammit.
I’m serving on the program committee for the 2018 Workshop on Principles and Practice of Consistency for Distributed Data, co-located with EuroSys ‘18 in Porto, Portugal. This will be my second time on the PC of PaPoC, a workshop that I like a lot.
Recently I remarked on Twitter, “I should donate to archive.org more. They’re how I know that large parts of my own past actually happened.” By “archive.org” I meant the Internet Archive, the organization that runs the Wayback Machine and many other projects. Here are three stories from 2017 about what I mean by that remark.
Something I really like about my blogging setup here on composition.al is that my posts are just plain old version-controlled text files. Years ago, Dave Herman remarked on how nice it is to be able to blog using one’s text editor, and I feel the same way. But there’s so much more to it than just being able to write my posts in my editor of choice. For me, the more important thing is that I can make use of the vast number of tools out there for manipulating text, including and especially versioned text. Because of that, I don’t have to wait for my blogging framework to implement this or that feature. I can just use tools that already exist.
This year, as I’ve started to dive into neural network verification, I’ve had the chance to learn a little about how SMT solvers are implemented. One thing I learned that surprised me is that under the hood, many state-of-the-art SMT solvers use the simplex algorithm to solve satisfiability problems.