The author has several articles about ATS (http://bluishcoder.co.nz/tags/ats/) and from what I've read, it outputs C code that is proven (for the parts that are in ATS) to be correct. There's a bit more detail in "Safer handling of C memory in ATS" (http://bluishcoder.co.nz/2012/08/30/safer-handling-of-c-memo...) and the end of the article contains some generated C code.