What's the highest level language, and why is it Idris?

>>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.