Ты конечно права, но есть неотъемлемый объём работы, который ты должна будешь делать в ATS, и который не нужно делать скажем в Хаскеле - я о доказательствах. Написание доказательств мне напоминает написание программ на динамическом языке с причудливым синтаксисом и без возможности отладки. То есть некий текст, который надо написать правильно для сигнатуры каждой функции, причём вход не всегда понятен, а выходом является сообщение об ошибке.
В Idris вроде довольно хорошая поддержка доказательств
Можно было бы хотя бы часто встречающиеся случаи покрыть, попробовать доказать дистрибутивность операции, инволюцию, инъекцию, попробовать скомбинировать это