Software I'm Thankful For

Last week I read Software I'm Thankful For and it inspired me to do a similar piece. I use a lot of different exotic tools, too, so I think it's a good way to share some stuff most people haven't seen. At least mainstream programmers, if you've been following me for a while a lot of this will be familiar.

TLA+ and Alloy

So let's start with the big, obvious ones. TLA+ and Alloy are both formal methods languages for finding problems in designs. It's something so outside the norm that many programmers don't even know that directly testing designs is a thing that exists, much less that it's economical and effective. I've met plenty of people who say FM couldn't possibly work, and then after a five minute demo switch to "I need to learn this right goddamn now."

That more than anything else is what makes me so optimistic about FM's long term future. Most developers have a well-founded skepticism of new or exotic technology. So to see people get excited so quickly? There's something really precious here.

(These days my favorite demo is an access control spec in Alloy. It's real simple and the counterexample visualizer is spectacular.)

TLA+ in particular changed the arc of my career. Up until 2017 I was Just Another Webdev. Writing about TLA+ got me my initial audience. Now I'm just as much known for software history and journalism as FM, but I wouldn't have gotten anywhere without the first step up. I'm grateful for that.

Neovim

"Why I'm grateful for Vim" isn't that interesting, so why Neovim specifically? Well originally it was for the async plugins and terminal emulator, which pushed vim to add those features, too. So even if I wasn't using it, it was good for the broader vim ecosystem. Then I switched specifically for inccommand, which shows you find-replace in realtime. This works even with regexes, which makes using them a lot easier.

Nowadays I'm really grateful for native LSP extension and the lua keybindings. As someone who lurves customizing everything, I've written a lot of Vimscript code, and the language is absolutely terrible. Neovim supports writing everything in lua, even your vim configuration files, meaning I can now do stuff like this:

local opts = { noremap=true, silent=true }
local copts = { noremap=true, silent=true, expr = true }
local function map(a, b, c) vim.api.nvim_set_keymap(a, b, c, opts) end

local nav_keys = {'h', 'j', 'k', 'l'}
for _, key in ipairs(nav_keys) do
  local c_key = '<c-'..key..'>'
  map('n', c_key, '<c-w>'..key)
  map('t', c_key, [[<c-\><c-n><c-w>]]..key)
end

That's about a million times better than using VimScript. That's also why we're seeing some incredibly cool plugins for Neovim, like telescope (a fuzzy-finder on steroids) and nvim-neoclip (fuzzy-find on clipboard history!)

AutoHotKey

When the m1 macs came out and blew all the benchmarks away I got really sad, because I feared that Windows laptops wouldn't be able to keep up, and I'd eventually become even more of an afterthought in the trendy tech world than I am now.

"Why stick with windows?" Because Windows has AutoHotKey, that's way! It's a full automation language that hooks into every part of Windows. Some of the things I've done with it:

• The Alloy IDE doesn't have an option to insert spaces instead of tabs, so I remapped <Tab> with <Space><Space>, but only when I'm in that specific IDE.
• Pressing del on the numpad (and only the numpad) switches my computer into "workshop mode", where clicking the mouse wheel left switches between class materials, class slides, and the IDE, and clicking the wheel right switches over to Zoom.
• When I'm in firefox, rctrl + ralt + s reopens the current tab in scihub, and rctrl + ralt + a opens it in the Wayback Machine. On youtube (and only youtube), [ rewinds the video back one second, instead of the normal five seconds.
• If I select a timestamp and press alt+` then it shows a popup with the time in UTC and Chicago time.
• Typing ;zoom puts in my personal zoom link.

I put some of my scripts up here. There's not a lot of great materials out there for actual software developers, which is a huge shame. The online community is nontechnical people, so you get lots of advanced tutorials explaining what "arrays" are. Doesn't help that the language itself is god-awful. Still, it gives me so much firepower I can't work on any other OS. I've tried both Mac and Linux for years, and in the end I returned to Windows just to get AutoHotKey back.

(I later learned that Mac has Hammerspoon, which I've heard is pretty good. Maybe one of these days I'll give that a shot— I miss Mac's file tags.)

J

I have a love-hate relationship with J. I feel like for any given problem, solving it in J will either be an order of magnitude easier or an order of magnitude harder than in any other language, and I'll have no idea which it will be. I've never really gotten my mind quite around it, even after five years, but I still use it anyway because hot damn when it flies it flies.

That's because J has absolutely incredibly arithmetic primitives. For example, if x is a 2D array, you could get the sum of all 3x3 subarrays of x with 3 3 +/@,;._3 x. It's like how people describe programming as "knowing the correct incantations", except here the correct incantation trivializes the problem. So I use J for lots of little analytic tasks. Most recently exploring Marsaglia's PRNG that fits in your head and revalidating some math of the Dunning-Kruger refutation.

What I really want is some kind of supercalculator, maybe a programming language + IDE geared entirely around arithmetic and combinatorics. Something where "remove duplicate elements including rotations and reflections" is easily composable out of the primitives, also things like "give me both g(x) and g(f(x)) and compare them" as core language features. J isn't this, but every other tool I've used isn't anywhere close to this.

Frink

Frink convinced me there's a huge untapped space for domain-oriented languages— viable as general purpose languages but targeted at a specific problem domain. In Frink's case, it's physical calculations. The syntax and a lot of the features are oriented around that. For example, x y == x*y. So you can do this:

half 1/3 cup -> [1/4 cup, tbsp, teaspoon]
0, 2, 2

So that's real nice for a lot of cooking.

Sphinx

I wrote learntla and Practical TLA+ in markdown, because that's what I knew about, and the experience convinced me I needed to replace markdown. Looking for errors meant poring over the text and manually checking everything, which was tedious and left a lot of mistakes. The most embarrassing mistake appeared early in Practical TLA+, where I wrote TRUE \/ FALSE = FALSE. And that got published. What I wanted was a way to automatically check all my code samples, ideally adding a tag to snippet saying "if run, it should get so and so" and tell me if that's not true. But you can't associate metadata content in base markdown; everything is either text or formatting information.

Indexing and references were also a pain. If I made edits it would change the paging of content, so I'd have to go through and update every instance of "see page XYZ". There's no way to put an anchor in the markdown text a la LaTeX's labels. So I started looking for a structured text format, which led me to reStructuredText and eventually Sphinx.

Sphinx is a documentation builder, originally designed for Python but now general purpose. It has whole-document cross referencing and allows customized structured blocks with options. This makes it much better for documentation than markdown-centric builders. For example, let's say I wanted to include some Python code. In CommonMark-style markdown, I could use a code fence:

```py
code goes here
```

and that's about it, I couldn't do anything more with it, like add line numbers. Various documentation engines that use markdown come up with their own flavored extensions to this, but they're all contradictory and none of them are extensible.

.. code-block:: py
  :linenos:
  :caption: name
  :emphasize-lines: 2,3,5-7

  code goes here

The important thing is that this code-block directive isn't part of baseline rST, but Sphinx added it through the standardized extension mechanisms. So the parser now knows about "code blocks" and rST editor plugins highlight and indent it as normal.

This means I can also add my own custom extensions and they're treated first-class. You can see a few I've already written for the new learntla here. Next I want to write is a "troubleshooting" block for marking out TLA+ issues and how to solve them.

Overall Sphinx makes documenting a lot easier.

ToupView

Not software related, but it's great for getting extreme closeup photos of things. Here's velcro:

Some thoughts

I notice that a lot of this software I'm grateful for has really sharp learning curves and high power ceilings. Probably says something about who I am as a person, and also why a lot of these tools remain fringe.

Not much else to say, just happy about software 'n stuff

If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.

My new book, Logic for Programmers, is now in early access! Get it here.