3 ms·
ats [http://www.ats-lang.org/ http://www.ats-lang.org/] is a C-level language with dependent types
by zem 8y ago
ats [http://www.ats-lang.org/ http://www.ats-lang.org/] is a C-level language with dependent types
- lodi 8y agoNote 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".