1. 13
  1.  

  2. 5

    What a coincidence, just yesterday I came across ATS again and figured it would be a good time to learn it. Anybody crazy enough to join me?

    1. 3

      I’m procrastinating learning ATS right now. Btw, how’s your followup to part 1 of “Reading Ur/Web signatures”?

      1. 1

        Yeah, about that… I kind of sketched out the ToC and then left it there to rot. I should finish that first, maybe refreshing my thoughts on it will help me with learning ATS, too.

      2. 1

        I saw the youtube video - while ATS strikes me as extremely interersting, I struggle to see a use professional use case for it. Would you mind to elaborate your motivation behind it, except, of course, intellectual cusiosity? I am already licking my wounds from my excursion into the jungles of Haskell, where Monads, Functors and other monsters bit me…

        1. 6

          In my case I used it for writing network services. I used linear types and proofs to help ensure program correctness and no memory leaks without a GC. Similar to what you’d use Rust for now, but with the ability to do proofs and dependent types.

          1. 3

            Hello,

            thanks for listing your project.

            Similar to what you’d use Rust for now,

            Could you give a comparison between ATS and Rust? My understanding is that Rust’s ecosystem and UI/tooling is way more developed, while ATS seems to give more freedom on how programs can be written. Or does Rust replace ATS in all function and form?

            1. 5

              Rust is definitely more developed and user friendly. Rust doesn’t replace ATS in that ATS has a more advanced type system. Things you need to do in unsafe Rust, like pointer arithmetic and dereferencing, can be done in safe ATS. ATS feels more low level - at the level of C but with an ML feel. ATS compiles to C so you can use any C compiler to use on another platform. Embedding C and calling C is easy. There are very few libraries though. I’ve written more about ATS here: https://bluishcoder.co.nz/tags/ats/

              1. 2

                Do you think ATS is used anywhere in industry? Drivers would be my first guess -

                That is quite an impressive post record. Thanks!

          2. 5

            A “professional use case” isn’t exactly what I’m after by learning it, but if you were to turn a blind eye to ergonomics and other stuff that supposedly could be fixed, I don’t think it’s such a hard sell. C with a great type system + all the nice ML features sounds like the best thing after sliced bread to me, and if I get to learn more about proofs and linear types in the process all the better. And even if I never get to use it I can still steal its ideas for the language I’ll never get around to implement.

            1. 2

              There’s a C compiler mathematically proven not to change program semantics when doing optimizations—CompCert. It’s the dependently typed language/proof assistant (Coq) that made that possible.

              I guess one problem with dependent types isn’t that they are inherently hard, but that they are not in the “mass consciousness”. Simple algebraic types and pattern matching are slowly getting into it, even though languages like Swift shy away from calling them what they are.

              At one point in hisroty, the concept of variables was revolutionary, but now it’s completely intuitive to everyone. Dependent types probably will be too.

            2. 1

              Good luck. I dismissed learning ATS after watching this video:

              https://www.youtube.com/watch?v=zt0OQb1DBko

              1. 5

                It’s not as hard as its reputation. Especially if you start with the ML side of things and slowly add dependent types and proofs as you get more familiar.

                1. 3

                  I’m watching that right now. My confidence comes from having already learnt Ur/Web, which is similar (derived from SML, bad ergonomics, arcane type system, lots of syntax, small community, sparse documentation, etc.) though a bit less threatening than ATS.

                  1. 2

                    Man, I loved that talk - one of my top 3 from that year’s strange loop.

                2. 0

                  When you give up on ATS, BTS is a good next step.

                  1. 3

                    In the same goal space, F* is also an interesting up and coming.

                    1. 3

                      Any pointer to BTS ? I cannot find anything

                      1. 2

                        Yeah, even I couldn’t find anything about it.

                        1. 2

                          BTS intro: https://www.youtube.com/watch?v=7C2z4GqqS5E

                          I’m sorry, I regret what I’ve done. :(