«Imperative programming in ATS is firmly rooted in the paradigm of programming with theorem-proving. The type system of ATS allows many features considered dangerous in other languages (such as explicit pointer arithmetic and explicit memory allocation/deallocation) to be safely supported in ATS» - http://www.ats-lang.org/
«The core of ATS is a call-by-value functional language inspired by ML. The availability of linear types in ATS often makes functional programs written in it run not only with surprisingly high efficiency (when compared to C) but also with surprisingly small (memory) footprint (when compared to C as well).» - 9000