To study algorithms, we first need to describe them. That’s what Turing did: the Turing machine is a description of all algorithms, built before most computers were even invented.

Types allow us to tell the compiler more information about our program, allowing for safer and more performant code. There’s a way to upgrade types and give the compiler even more information, and it’s using dependent types.

As programmers, we spend our days battling the enemy. The enemy is tough, devious and sneaky. The enemy entrenches itself into your own lines (pun not intended) only to be found when it’s already too late. This enemy is complexity. But fear not! There is a way to fight it!