Posts

Last weekend I had a conversation with an undergraduate student new to computer science, who was reading CLRS. “I wish” they said, “that all the pseudocode in my algorithms textbook was just written in Python.” “Ah” I said, “but textbook authors sometimes want their work to endure beyond a decade.” “But Python’s been around for a long time” came the reply, “and it’s very readable, and you can’t execute pseudocode anyway so what’s the harm?”

An unusual topic for this blog, but worth boosting to a larger audience: Google Groups is dying. Its epitaph is not yet inscribed on the Killed by Google website, but the end is easily seen from here (although it should also be noted its death was called as early as 13 years ago). The deficiencies in Google Groups search, supposedly Google’s forte, have long been noted. Lately though basic features have just stopped working.

A few days ago I published a short post about two bugs I wrote while developing the C++ external scanner for my TLA⁺ tree-sitter grammar. Reactions were mixed! Many people were supportive, but there were of course the usual drive-by claims by developers that the bugs were trivial, they would’ve found & fixed them inside of 20 minutes, and I was laughably incompetent for having written them in the first place. Maybe so! I’m a fan of formal methods primarily so I don’t have to be a genius to write correct code. In that same vein of building tools to save us from ourselves, one user suggested building the tree-sitter grammar with the LLVM address & undefined behavior sanitizers enabled. I’d used valgrind a long time ago but had never played around with sanitizers. I was also doing some closely-associated work to build the grammar for fuzzing with LLVM’s libFuzzer, so it seemed a fun detour to check whether those sanitizers would have saved me days of debugging pain!

Here’s a short post about two bugs I wrote while writing C++ code for the external scanner of my TLA⁺ tree-sitter grammar. External scanners use handwritten C or C++ code to parse the non-context-free parts of your language. I’ll try not to dump on C++ too hard but both of the bugs are highly ridiculous and exemplify why I hope to write as little of the language as possible for the rest of my career. These aren’t bugs with C or C++ themselves (although honestly this point could be argued) but I share them in the hopes someone finds entertainment in my misery.

2021 saw the completion of my first substantial free software project: a TLA⁺ grammar for tree-sitter, the error-tolerant incremental parser generator. The project stabilized & found users over the course of 2022, then over the holidays I used it to build the TLA⁺ Unicode Converter. The new year is a time to reflect on the past and look to the future, so here in early 2023 seems ideal to publish my experience.

Both TLA⁺ and tree-sitter itself ensured the project was fascinating on a technical level; even more interesting were the social and psychological aspects of my first real involvement with the free software community! I’ll go over why I wanted to create this project and the main technical challenges I faced doing so, then discuss the conditions that enabled me to create it and how free software development changed the way I think. If you’d rather get the technical part in video form (with demos!), you can watch the presentation I gave at TLA⁺ Conf 2021 (slides: pdf, odp):

Author’s note: I wrote this in 2017 and it languished in the drafts since then because I couldn’t think of a good conclusion. Really this is typical of the subject matter and all this piece offers is something to chew on, if you have the interest in it or have never before considered the question. At the time I was helping tutor a TLA⁺ seminar and had the opportunity to ask Leslie Lamport (who has thought about computation quite a bit!) what he thought of the question with all his accumulated wisdom, and he replied “it’s one of those meaningless distinctions, like the difference between alive and not-alive.” So there you have it. Hopefully there are enough decent jokes in this post to make it worthwhile.

It’s hard to find a textbook series garnering more effusive praise than The Little Schemer, The Little Prover, The Little Typer & co. The Little Typer introduces dependent type theory and is the first of the series I’ve read. I quickly grew to appreciate & enjoy its dialogue-based presentation - I’m a real convert! I might release future didactic blog posts as a dialogue rather than straight recitation of material in block paragraphs. Humans seem to naturally find conversations more interesting than the traditional lecture format of a single voice droning on, which might explain why comment sections often get more traction than the actual article being commented upon! Or the popularity of topic podcasts versus lecture series.

Republished from Teleport’s official blog (link). I received compensation from Teleport for writing this post.

Z3 is a satisfiability modulo theories (SMT) solver developed by Microsoft Research. With a description like that you’d expect it to be restricted to esoteric corners of the computerized mathematics world, but it’s made impressive inroads addressing conventional software engineering needs: analyzing network ACLs and firewalls in Microsoft Azure, for example. Z3 is used to answer otherwise-unanswerable questions like “are these two firewalls equivalent?” or “does this set of network ACLs violate any security rules?”

Interpretations of quantum mechanics are boring. Boring! Maybe the universe has a strict partition between quantum and non-quantum. Maybe there are a bunch of parallel universes with limited crosstalk. Or maybe it’s whatever the Bohmian mechanics people are talking about. Shut up and calculate, I think. I don’t say this out of some disdain for idle philosophizing or to put on airs of a salt-of-the-earth laborer in the equation mines. It’s just there are so, so many interesting things you can learn about in quantum theory without ever going near the interpretation question. Yet it’s many peoples’ first & last stop. Rise above!

In which I am stunted upon by coin flips

Wasn’t too long ago that I felt pretty good about my knowledge of distributed systems. All someone really needed in order to understand them, I thought, was a thorough understanding of the paxos protocol and a willingness to reshape your brain in the image of TLA⁺. Maybe add a dash of conflict-free replicated datatypes, just so you know what “eventual consistency” means. Past that it’s just some optimizations and mashups which come easily to your TLA⁺-addled brain.