"A Little Taste of Dependent Types" by David Christiansen
In brief
David Christiansen gives a Strange Loop 2018 introduction to dependent types, where one language serves for both compile-time and run-time code and programs unite with proofs. It draws on his book The Little Typer.