Щас ВП неистово надрачивает на Скалу™ и Монады™ (Хаскеля что показательно не трогает) - и учыдэтомушкубентов как "переднему краю науки" на языках с системой типов первого порядка (в чем по крайней мере Хаскель упрекнуть низзя).
Так вот - позволю понострадумусить:
Щас будущее за ATS2 (и смежными вещами типа Agda/Idris) - не потому, что на нем все скоро будут писать (не будут скорее всего - он слишком "барочен" и ad hоc для этого) - а потому что через 10 лет все сколько-нибудь актуальные идеи будут восходить именно к нему. И ВП опять (если не помрет к тому времени) будет "учить студентов зависимым типам на Idris/..."
Такие дела.
PS: Да - первое ознакомление - лучше всего Idris - главное не пытайтесь на этом реально что-то писать - но именно как первоначальное введение - самое то. ATS2 - это что-то типа С++ нового времени. Со всеми плюсами и минусами - очень сложный и нафичканый язык. Но при этом как и С/С++ - управляемый всем до самого нижнего уровня