Comment by doublec | Hacker News Reader

Comment by doublec | Hacker News Reader

Parent Full thread

If you use the non-dependently typed parts of ATS it is no more verbose than most ML variants. If you use it without the GC then verbosity increased because you need to add calls to free memory. If you add proofs or dependent types then declaring those adds more. I've used it in moderately sized production programs and it's similar to using OCaml or other ML in terms of productivity. Once you're familiar with the language of course.

If I paraphrase what you said about Haskell it's true for ATS too:

    "but one of the lovely things about ATS is that despite its reputation as a difficult language, once certain key concepts are tackled, it's relatively easy to program rapidly and create real world products (with a considerably higher assurance of correctness than most languages provide)."

The key, like any language, is learning the concepts. I think people assume ATS is more difficult than it is is because much of the documentation and examples for it use a verbose style and heavy proofs. A post I wrote a while back attempts to gently introduce ATS dependent types and you can see that the non-dependently typed examples are very similar to any other ML language:

http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.h...

> If you use it without the GC then verbosity increased because you need to add calls to free memory

The issue is that is the default mode I would like to work in. Rust is designed to make that the natural mode of working, rather than the exception. Fast, deterministic operations should be easier and more succinct than the managed alternatives – in the context of a systems language that is.

> people assume ATS is more difficult than it is is because much of the documentation and examples for it use a verbose style and heavy proofs.

Then they need better docs. And a better website! And better marketing!

It's interesting looking at the different design decisions of languages. One persons pro is another's con.

ATS2 has no GC as the default mode of working too. The only reason it is more verbose is because you need the call to free. ATS strives to be explicit in what it does so it's easier to read the code and know what is happening.

Languages with destructors or implicit function calls seem to lean towards the C++ downside of "What does this code really do" when looking at it. I dislike hidden code where there is no easily identifiable call to tell you something is happening.

It's not all roses and unicorns with ATS either of course. What I really want is the next generation of dependently typed system languages which has learnt from the current ones.

> you need the call to free

So how does ATS enforce memory safety? With Rust you have a bunch of library types that you can reuse that abstract away from the memory management for you. The types make sure you don't screw up. Unfortunately you can't prove things about the `unsafe` blocks, and have to rely on careful auditing, but that only needs to be done once, and then you have a nice, reusable abstraction. Bookkeeping sucks.

> What I really want is the next generation of dependently typed system languages which has learnt from the current ones.

Agreed. At the moment Rust suits me the best, but I definitely don't think it is the end of the road.

> So how does ATS enforce memory safety?

Linear types. Much like unique pointers in Rust, the type system tells you when you fail to consume a linear type. A 'free' call would do this. Same with closing files, etc - you use linear types to track that the resource is consumed.

Ah neat. Does it have regions?

And to be clear, ridiculously verbose, dense, and unreadable proofs is the UX failing of most DT languages today. My understanding is that ATS is not significantly better or worse in that department.

Reply on news.ycombinator.com