1. 22
  1. 5

    Whiley is a really interesting project. David, I really like your paper “Sound and Complete Flow Typing with Unions, Intersections and Negations”. I’ve found much use for its ideas several times in the past year. Thank you.

    1. 2

      Wow, I wish I had known about this paper a year and a half ago, when I was trying to re-invent this, for an early prototype of Dawn. Looking forward to studying and implementing a prototype concatenative language using this.

      1. 1

        Hey, thanks!! Great to hear someone actually read it :)

        1. 2

          Hey, question for you: Have you thought about how flow typing could be combined with compilation to machine/object code? You could of course assign a unique type id to each type, but that would have to be done at link time, presumably, and then it’s not clear how dynamic linking could work. Any thoughts on this problem?

          1. 1

            Hey, so your question seems connected with low-level representation of flow typing. Yes, I have thought about this. Probably my preferred solution is actually to use type tags. So, a type like null|int has a one bit tag to distinguish null from int. However, this then raises separate questions, as to how map arbitrary combinations of unions and intersections (as in the paper) down to this. Happy to talk more about it!

            1. 1

              Okay, interesting. I had considered that, initially, but then thought all the conversions between encodings would be too expensive. But maybe the compiler could choose encodings so as to minimize conversions, at least within a procedure?

              1. 2

                Hey, so yeah … this is a key question. I have thought about it a bit, though not made any specific decisions. You are right that you’d want to minimise conversions. I also agree that some conventions could be used to minimise the coercions, or at least make them efficient. Anyways, yeah, needs thought :)

      2. 3

        Oh wow, that looks possibly really interesting to me, kinda like something similar to Dafny but not dead? I.e. formal methods with syntax consumable by a (relatively) common programmer that is me. Will try to see if I can manage to understand it enough to try proving something simple.

        By the way, what’s the memory management story, especially when compiled to C? Didn’t seem to see it explained at first glance. Also, did you see the Nim language’s (unfortunately dormant AFAIK) “Dr Nim” project?

        1. 2

          Dafny definitely isn’t dead. Amazon is using it for example, though I’m not sure exactly what for.

          1. 1

            to Dafny but not dead? I.e. formal methods with syntax consumable by a (relatively) common programmer that is me. Will try to see if I can manage to understand it enough to try proving something simple.

            Have you tried Why3? It’s the closest to Dafny. (I think both are actively maintained?)

            1. 1

              (I think both are actively maintained?)

              Oh, interesting, you seem to be right! I wonder why I had a different impression; maybe I looked at it at some really unlucky time? And apparently Dafny can now compile to Go and JS, very interesting too, thanks!

              1. 3

                The maintainer of Dafny, Rustan Leino, left Microsoft Research a few years ago. But Rustan Leino keeps working on it at Amazon, which basically seems happy to fund any formal-methods work as long as it gets applied to their codebase.

          2. 2

            Seems like a sensible RIIR (tiny, well defined interface, replaces JVM startup time with something native can shine..) that won’t crash and burn in two weeks ;)

            If I find the time I’d like to compare how different whiley is for example from spin and JML. It looks saner.