What's the highest level language, and why is it Idris?
>pure functional
>dependent types
>proofs
>totality checker
>>62121697
>high-level
>good
>>62121697
Shen is also a good contender, you can write your own type system in Gentzen sequents.
But as >>62121792 hinted, there seems to be some sweet spots for usability. I used to like one of these where the language is type-safe and Hindley-Milner type inference is feasible--this is Standard ML. When you go beyond that, e.g. ATS, I find it very difficult to keep track of all annotations, syntax and semantics.
On the other hand, I've seen research support the thesis that a strong & safe type system only has a marginal effect on quality. I found this personally disappointing, but you can't argue with facts. Automated test harnesses seem much more effective. So I'm not as interested in type systems as I used to be, and write a good lot of Forth these days.