1. 24
    1. 18

      Just a small somewhat OT note:

      All in all the experience has given me a serious love/hate relationship with type theory and comp sci papers, mostly verging on the “hate” side. On the one hand, if I replace the variables â and â’ in your algorithm with paramtype and rettype and then go “…wait, is THAT what it’s doing? That’s all? Oh.”, then you’re failing as a communicator.

      \rant{ YES. I find math in CS papers frustrating because of its ubiquitous usage of single-letter names for everything. They’re difficult to remember, and I hate having to go back several pages to remind myself what they defined W as, or what the ζ operator is supposed to represent.

      All coding style guidelines (except maybe APL’s) discourage single-letter identifiers, outside of trivial cases like loop variables. Why should academic papers hold onto a convention whose purpose was to conserve chalk and pencil lead? }

      1. 5

        There have been a few books over the years that teach mathematics using a programming language, and I rather enjoy them.

        The Haskell Road to Maths and Logic is one. Coding the Matrix is another.

        1. [Comment removed by author]

      2. 2


        Because otherwise you can’t pass the peer-review, imagine if they were able to verify that and find out it doesn’t actually do anything new ;)

      3. 1

        Why should academic papers hold onto a convention whose purpose was to conserve chalk and pencil lead?

        I think this is a common misunderstanding of this practice. I would say the purpose is to keep the syntax as small and unobtrusive as possible so that you can a) focus on semantics, and b) fit as much as possible in your head at once. There’s also the aspect of making it easier to manipulate the symbols, to ease exploration.

        There’s certainly a tradeoff in terms of the slope of the learning curve, but when conventions are shared among a group of active researchers, it more than pays for itself. But it does make it harder for outsiders to break in. That seems to be a fundamental tradeoff, though, at least at some level, between optimizing for beginners vs optimizing for experts.

        1. 1

          But what is so different about math, that it overrules all the very good arguments made against single-letter identifiers in programming?

          Especially the argument that “your code is going to be read many more times than it’s written, so clarity at the expense of a few more keystrokes is a good tradeoff.” Because the whole point of an academic paper is to be read and understood.

          I would agree that common constants, variables and operations — like pi, or c in physics, or O() in CS — work fine as symbols. But when you make up an identifier for a specific local purpose, a name is so much better.

          1. 1

            A few disjointed thoughts:

            1. Mathematical notation long predates programming.
            2. Verbosity doesn’t always improve clarity. In fact, the opposite is often the case, e.g. Java.
            3. Single letter variables are fairly common in Haskell, especially in small helper functions that are best understood by their semantics.
            4. As long as you clearly define your notation, I don’t see how a longer identifier, e.g. OrderOfComputationalComplexity(n), is better than a short one, e.g. O(n). Unfortunately, it’s not particularly common for journal articles to specify which notation they are using, but rather to assume the readers general familiarity with the existing literature and notations, which forces newcomers to detour through introductory text books and/or review articles before they can understand the latest articles.
      4. 1

        Mostly because of archaic university standards that impose a page limit on the paper.

    2. 5

      I love this, keep going. Thank you for building in public.

      Math has never been my friend but I know I shall bend it to my cruel whim sooner or later. Always have before.

      Also, this is such a great attitude.

    3. 4

      I love this idea. Please - if I may throw in my 2c -make all borrowing interfaces explicit. That means explicit annotations with parameters of the capability/ownership level required and avoid lexical capture (because that’s implicit borrowing which is the worst).

      1. 2

        You mean for closures, or for some other kind of expression?

        1. 2

          I mean, every time something passes to a place where borrowing or ownership needs to be checked, it should be via explicitly annotated parameters. Which I think means you couldn’t have closures but could have eg object expressions or lambda expressions.

          In my opinion it’s one of the nicest things about pony. The way pony explains it is perhaps a little hard to understand initially. I think rust optimizes for spreading the pain over time rather than taking the pain briefly and up front in learning what the annotations mean. Explicit is better than implicit is probably the most enduring lesson I take from Python.

          1. 5

            If I’m understanding correctly then you mean something like explicit lifetime annotations? I’ll check out Pony to see how it works, thanks for the suggestion.

            1. 1

              Well, that sounds like another good idea ;)

    4. 4

      What to use for its backend, though? There’s not actually that many general-purpose compiler backends out there, your choices are basically GCC or LLVM, and both of those are large hulking monsters I would really prefer not to have to deal with.

      Would Zig’s self-hosted compiler theoretically be an option here?

      1. 4

        Possibly? I don’t know if it’s designed for the backend to be reusable in other projects.

        1. 1

          There’s also qbe, which is meant to give a large amount of functionality to a backend, in a small amount of code. It’s relatively approachable and has an LLVM-like language, without being a “large hulking monster.”

          1. 2

            Yeah, I’m aware of it. I’m not sure it’s mature enough I’d want to rely on it yet, but it is what first made me think “…okay, maybe I don’t need LLVM or a comparable-sized project”.

    5. 3

      Not much more that I can say than: 💕

    6. 2

      I did accidentally reinvent bidirectional type checking, which is cool

      I love this kind of openness, those are the things you giggle about when you realize them at 3AM sitting in front of your “solution”.

    7. 2

      There is a Never type which works way better than I ever expected

      Is this a secret plot to speed up stabilization of the ! type by rewriting Rust?

      1. 2

        No, Rust’s current ! type works pretty fine for what I need it for.

    8. 2
      Borrow checking

      Okay I have to admit I have no idea what I’m doing here, at least in a formal sense.

      I hear this page has some good resources for those trying to understand the workings of Rust.

    9. [Comment removed by author]