1. 29
  1. 6

    I came upon this project through a blog post linked via This Week In Rust, and I found it fascinating. The author’s goals and motivations, and even some aspects of his approach, align very well with what I’m working on with Dawn.

    1. 2

      Dawn looks interesting. I like the multi stack idea.

    2. 4

      Academics aren’t incentivized to create something like this, because doing so is just “applied” research which tends not to be as prestigious. You don’t get to write many groundbreaking papers by taking a bunch of existing ideas and putting them together nicely.

      I disagree on this. At least in the UK, there’s an exercise every few (typically 5) years that ranks all of the university departments (it used to be called the Research Assessment Exercise [RAE] but that actually conveyed meaning and so it was renamed the Research Excellence Framework [REF]). This directly affects the amount of funding departments get and individual contributions to the input for the rankings thing has a big impact on academic promotions.

      The REF is supposed to look at impact and it evaluates artefacts other than just papers. A tool that enjoys large-scale deployment in industry gets you a lot of points in the REF. If it is relatively easy to take the research ideas and turn them into a language that everyone uses, then there are enough incentives to do this in academia. There are even special categories of grant available for this kind of activity.

      Writing a dependently typed language that performs well and scales up to very large codebases is incredibly hard. It’s great to see people trying this because dependently typed languages are amazing to use and if you can write one that performs well on codebases that are a few millions of lines of code then that’s an incredibly valuable contribution, but don’t assume academics aren’t trying to do this. They are, it’s just that the problem is really, really hard.

      1. 1

        Yeah, this post is a statement of intent, but he doesn’t have any examples or prototypes or anything that would indicate he’s actually made any progress. And he doesn’t seem to understand the current FM landscape, like why these are hard problems in the first place!

      2. 4

        It’s not directed at Magma but I noticed that most proof-related discussions seem to ignore ATS for some reason. Maybe the language is too unsexy to be interesting to developers?

        1. 2

          ATS

          I didn’t even know about this. Very cool, thanks for the pointer.

          1. 1

            yeah I am also quite interested in ATS it is a very interesting approach.

          2. 2

            Strange. I’m getting 500 errors on Github.

            1. 2
              1. 1

                Github seems down for everyone