First let me say that I have not written anything substantial in ATS. I have been pondering what it can be used for for a long time. I think ATS has some really

First let me say that I have not written anything substantial in ATS. I have been pondering what it can be used for for a long time. I think ATS has some really neat features. It is almost two languages combined into one from a practical point of view: 1) An ML style language. 2) A linear type based imperative language. On the plus side it has strong theoretical foundations; compiler code base is small enough to be readable; it transpiles to everything and has top notch performance at least for the C target using the second style. The catch is that I would like to write code in the ML style, which requires GC for long running programs (the ATS compiler itself does use the ML style without GC as memory leak is not a concern for a batch mode application). That makes it hard to start small with a library project. The linear type style is high performance but a lot more challenging to use. Xi encourages users to start with ML style and transition into the linear type only when needed. I have experience doing proofs (group theory in math) using a dependent type prover (Lean). Tooling is really important. Even with excellent type feedback one really needs a lot of automation (like integrated SAT provers) to make the work practical. My feeling about the linear type is the same. We need the proofs to be mostly automated and a lot of nice feedback when the type checkers fail for it to be practical. Though if safety and efficiency are both critical someone may be willing to pay the price now to use linear types. So maybe it will have good applications in the embedded software domain. In my interest area resource usage is only a (small) part of the concern. Even if one roots out all resource bugs one still has logic bugs to deal with so the the availability of and the ease to use well tested libraries are a lot more important than resource management to me. This has been a really promising language project. If it gets some well-deserved community love maybe it will really blossom.