My experience may be too specific to reason about productiveness with ATS when it comes to other developers. I knew some Haskell and I've already read the Idris

My experience may be too specific to reason about productiveness with ATS when it comes to other developers. I knew some Haskell and I've already read the Idris book when I discovered ATS, and I knew some C from university courses. The proofs require the same mental model, totality check principles are the same, resource utilisation principles are the same, so for me the difference when comparing these two langauges is mostly about the things available apart from the common features: ATS prelude has many predefined constraint functions that facilitate low-level programming with pointers over unboxed data. I haven't tried F*, but from quick googling of "aliasing", it seems that a similar kind of checks can be achieved with view-changes in ATS (but please correct me if I'm missing the point) - http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3756.html http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/...