First, some background: I’ve been busy working on CrossHair lately. It uses symbolic execution to check properties of Python programs. Z3 is a popular SMT solver (kind of theorem prover) that CrossHair uses.
As of the last week or so, CrossHair can check properties of Python programs using regular expressions. You can fiddle with an example in the CrossHair playground, here. Below, I ramble about my adventure in making this work.
Z3 has some native support for regular expressions. Initially, I thought this would work to model regular expressions in Python. …
CrossHair uses Python objects that look like native values (ints, lists, etc). When these values are passed to functions implemented in C, a variety of things can go wrong, which is why CrossHair monkey-patches some of the standard library during evaluation.
To figure out what of the python standard library to prioritize I did a quick survey of module popularity. My methodology wasn’t amazing — I’ve left those details at the bottom for the interested. And without further ado, the list:
| module/package | references (thousands) |
I’ve just finished the v0 of a simple turn-based strategy game, EmojiTactics. You can play it here: [mobile /desktop]. It’s similar in spirit to Hearthstone or Magic: The Gathering. It also has a curious property: every graphical element in the game is an emoji. This post rambles a bit about that and other dev topics that you might likely find boring.
Apart from helping make the game tiny, using emojis has other odd consequences. One of these is that the game looks and feels quite different depending on what platform you’re using:
From compilers to web apps, databases to caches, maintaining computed state is the most prevalent and thorny problem I’ve faced as a developer. Most of this article is about that problem, but skip below to “A Tiny Contribution” if you just want to see some code.
Many of us developers are familiar with this famous quote from Martin Fowler:
There are only two hard things in Computer Science: cache invalidation and naming things.
Cache invalidation is an incredibly hard thing to get right, to be sure; but that’s not the point Fowler is making. …
4/29/2016 edit: Feel free to play with the code I’ve written to perform these transformations (in a very strange language called Maude): https://github.com/pschanely/wf-optimizer
Much of my independent-thinking life has been consumed by questions like this: How do we make compilers smart enough to know that “sum(reverse(x))” can be rewritten to “sum(x)”? Or that “reverse(reverse(x))” can be rewritten to “x”? Without special knowledge of what “sort” and “reverse” mean, these are challenging problems. I don’t know of any popular compilers that make these optimizations on their own. (please tell me about it if you know of one!)
Just recently, I noticed…
The traditional search interface, with its array of filters, facets, and sorting options is ubiquitous. It also sucks. An explanation might not have been required, but for a suspicion of mine. A suspicion that databases have spent the last few decades training us. They’ve been training us to think about search in ways that are easy for them to implement.
It’s time to remind our databases that they work for us.
To illustrate, consider the task of finding a used car. The data looks like this:
If you’re like me, you filter on mileage, and then sort on price, lowest…