Note that ATS has a limited version of dependent types as compared to Idris/Agda/Coq/etc. As I understand it, you can't run arbitrary (recursive, etc) function

Note that ATS has a limited version of dependent types as compared to Idris/Agda/Coq/etc. As I understand it, you can't run arbitrary (recursive, etc) functions at the type level. But even this 'lite' version lets you express preconditions like "n is a multiple of 4" or "the source array and destination array must not overlap in memory".