Last night, while I was catching up on email, I wanted to make use of my time and our Claude subscription. I decided to scratch an old itch.
Our aeon programming language has Liquid Types (e.g., {x:int | x > 0}) and we rely on an SMT solver to type check the implications of subtyping (e.g., when passing something of type {x:int | x > 3} to a function that accepts {x:int | x > 0}, we need to verify whether x > 3 -> x > 0, for all x).
But there was an issue: aeon is written in Python and relies on the z3 bindings that contain C++ code. We can run Python code in the browser with Pyodide, but the native libraries are not directly supported (at least this one, that relies on multi-threading).
On the other hand, there is a z3 port to web assembly (by alectryon’s Clément Pit-Claudel, no less) but it follows the C API, and has no browser-Python bindings.
So while I went through the ivory tower tall pile of emails, Claude reimplemented the z3 bindings in a different package, used the export to SMT-lib format feature, already present in z3, and passed that to the z3-wasm package.
I asked for examples, and piping the errors I found in the browser back to Claude, I gave up on being a middle man, and instructed Claude to use Rodney to interact with the browser directly (I was running this on a linux server, not my local machine). It then went ahead and made the examples work on Chrome, in a nice demo page. Unfortunately, it did not work on Safari due to the lack of stack switching support in web assembly, so I needed to make another prompt to fix that issue. It deployed to GitHub and Pipit automatically, with little effort.
Of course you get what you paid for: I provide no assurance that there are no bugs. But it’s useful enough for me to prepare some demos and materials for students that do not require any installation or compilation in their machines. That’s a win in my book.
And now, you have support for z3 in Python within the browser for your existing z3 Python projects, or just to play with z3 because the Python bindings are by far the most easy to just play with.