About the Book

You can purchase this book on Apress

Dependent types are a powerful concept that allows us to write proof-carrying code. Idris is a programming language that supports dependent types. We will learn about the mathematical foundations, and then write correct software and mathematically prove properties about it.

This book aims to be accessible to novices that have no prior experience beyond high school mathematics. Thus, this book is designed to be self-contained.

The reason for writing this book is that I could not find a book that explained how things work, so I had to do a lot of research on the internet through white-papers, forums, and example code in order to come up with a complete picture of what dependent types are and what they are good for.

The first part of this book serves as an introduction to the theory behind Idris, while the second part is a practical introduction to Idris with examples.

Contributions to the book are welcome on GitHub.

About the Author

Boro Sitnikovski

@BSitnikovski

Boro Sitnikovski has over 10 years of experience working professionally as a Software Engineer. He started programming with the Assembly programming language on an Intel x86 at the age of 10. While in high school, he has won several prizes on competitive programming, varying from 4th, 3rd, and 1st place.

He is an Informatics graduate - his Bachelor's thesis was titled "Programming in Haskell using algebraic data structures", and his Master's thesis was titled "Formal verification of Instruction Sets in Virtual Machines". He has also published a few papers on software verification. Other research interests of his include programming languages, mathematics, logic, algorithms, and writing correct software.

He is a strong believer in the open-source philosophy and contributes to various open-source projects.

In his spare time, he enjoys some time off with his family.