> 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.
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.
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.
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!