Type-Driven Development / Idris 1

Introduction

Hello programmers and mathematically inclined folks of steemit!

In the second half of this year, I will go through the newly released book Type-Driven Development with Idris, thereby introducing coding with a purely functional dependently typed programming language.

Dependent types have a bunch of ramifications. I initially became interested in it because of the Curry-Howard correspondence, enabling one to use constructive formal logic - which is conventionally used to express set theory and bootstrap all of mathematics - at the type level. But there's more...

As a side note, In my second post I had just asked about code presenting practices on steemit, to make this a proper series, and I'm thankful for pointers.

Take care!