ATSは依存型言語の中でも奇抜な方だと思うよ
Coqとソフトウェアの基礎の方が易しいと思う