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