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.
Halide is a newish domain-specific language for writing high-performance image processing pipelines, originally created by a group of researchers at MIT and Adobe and now used in lots of places. Although the original paper on Halide appeared at SIGGRAPH 2012, I like the PLDI 2013 paper better as an introduction to this line of work.
Halide is really two languages: one for expressing the algorithm you want to compute, and one for expressing how you want that computation to be scheduled. In fact, the key idea of Halide is this notion of separating algorithm from schedule.
Between mid-2015 and mid-2017, I spent a lot of time on performance measurement for the ParallelAccelerator package for Julia. I curated a collection of workloads of interest and tried to automate the process of benchmarking them as much as I could. Many of the workloads had originally been written in Matlab or Octave, and the Julia versions had been ported from those.
A couple months ago, Jean Yang started a crowdsourced list of women doing programming languages and software engineering research. I added my name and advertised the list in a couple of communities I’m part of, mentioning that although I think there are upsides and downsides to such lists, on balance I think they’re good. A friend asked me to elaborate on what those upsides and downsides are.