Собрал небольшую подборку видео о программировании на Idris — языке с зависимыми типами, которому не помешает щепотка популяризации.

https://www.youtube.com/watch?v=X36ye-1x_HQ — доклад, с которого для меня всё началось: Эдвин Брэйди, автор языка, рассказывает, что такое вообще Idris и какие преимущества он может дать программисту.
https://www.youtube.com/watch?v=4i7KrG1Afbk — отличный доклад Брайана МакКенны о практических применениях Idris без единого примера сложения векторов, ура!
https://www.youtube.com/watch?v=DRq2NgeFcO0 — выступление Эдвина Брэйди о нововведениях в разрабатываемом сейчас Idris 2 — в частности, о Quantitative Type Theory, которая позволяет выражать количество «использований» (consumption) аргумента функции.
https://www.youtube.com/watch?v=QMPum88xluE — доклад от Сьюзан Поттер о работе с AWS при помощи Idris. На мой вкус, слишком много времени уделено детальному разбору соответствия Карри-Ховарда, но часть про работу с AWS прекрасна.
https://www.youtube.com/watch?v=AWeT_G04a0A — доклад от Дэвида Кристиансена о представлении паттерна универсумов в Idris на примере программы по работе с изображениями.
https://www.youtube.com/playlist?list=PL-_cKNuVAYAXFRLj6n2nDjI1cyHjuI3HI — ну и куда же без цикла лекций от Виталия Николаевича Брагилевского (@bravit_about), где язык разбирается с самых азов по книге Эдвина Брэйди «Type-Driven Development with Idris».