I haven't used ATS. My understanding is that it's a dependently systems language which makes me think it'll provide good region types and things like what Rust

I haven't used ATS. My understanding is that it's a dependently systems language which makes me think it'll provide good region types and things like what Rust is trying to offer. In that way I'd say it still differs a lot from, say, Agda, where you're likely to encounter fairly heady questions about equality and algebra very quickly. But again, I've not used it so I can't much say for certain.