Подскажите перспективный ЯП, которому требуются батарейки

Idris.

+ Lean, F*

+1!

Перспективные, конечно, Idris/Agda.

Остальное упомянутое здесь на мой взгляд рост «вширину». Т.е. «ну ещё один такой же язычек только вот мы тут записываем по-другому» (как крайний случай «по-другому» - на русском). Кроме разве что раста который ввёл лайф скоупы или как там они. Но «лайфскоупы» нам в хаскель/идрис завезли в виде линейных типов. Причём, кстати, в идрис они не допилены до юзабельного состояния вроде.

вот ссылочки на предмет чего поделать в идрис, здесь общее описание: https://www.idris-lang.org/help-required/ , а здесь то что по мнению разработчиков является «низко весящими плодами» (Low Hanging Fruit, в смысле требуют наименьших усилий для реализации) https://github.com/idris-lang/Idris-dev/issues?q=is:open is:issue label:"C-Lo...

Доб. вот тут ещё один список есть, с описанием и как раз тем, похоже, что ТС хотел бы https://github.com/idris-lang/Idris-dev/wiki/Contributions-Needed