A different, more imperative approach:
A paper algorithm notation, by Kragen Javier Sitaker.
I tried writing a suffix tree class with Kragen’s paper algorithm notation the other day. The problem is that suffix trees have many nested layers of ifs so I ended up running out of horizontal space and then getting frustrated. I barely understand suffix trees well enough to hold them in my head, so I’m thinking I should start by writing out something I understand better. That’ll separate the concern of developing muscle memory and fluency for the notation from the concern of improving my understanding of suffix trees.
As a side note, writing a suffix tree in J would be even more painful.
The ending was really nice!
I noticed that the author mentions TLA+ on his about page and was surprised he didn’t mention it in the post. For the lobsters users who have some experience with TLA+, does it lend itself to being handwritten? I understand it’s not equivalent to code logic, but I’m curious.
It’s pretty easy to write TLA+ operators, especially given the number of mathematical symbols it uses, but I wouldn’t say it’s better handwritten than typed. Operators are somewhat harder, pluscal and models are moderately harder. In contrast, I find it a lot easier to write J programs by hand and then type them up vs typing them in from the start.
Thanks for the reply. I went and read one of Lamport’s papers where he describes TLA+  in the meantime and it seems like there’s another benefit to working with TLA+ on the computer, the ability to drill-down or up on sections of a proof. Not sure how big a difference it makes in practice.
Oh, the big benefit to writing TLA+ on the computer is that you can use the TLC model checker to find spec violations, which IMO is what makes TLA+ worth learning in the first place. Having a clean way to express systems one thing, having a clean way to validate them is quite another.