1. 34
  1.  

  2. 6

    A different, more imperative approach: A paper algorithm notation, by Kragen Javier Sitaker.

    1. 1

      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.

    2. 3

      The ending was really nice!

      1. 1

        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.

        1. 2

          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.

          1. 1

            Thanks for the reply. I went and read one of Lamport’s papers where he describes TLA+ [0] 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.

            [0] http://lamport.azurewebsites.net/pubs/proof.pdf

            1. 1

              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.