Programming with dependent types in Idris

Building robust software is a hard task these days. As software gets more complex it gets increasingly hard to reason about it, this leads to a larger attack surface for bugs and security flaws. Some of these bugs can be completely eliminated with the introduction of type systems that keep our values at runtime in check. Type systems are in fact the most widespread mechanism to verify correctness properties of programs, with dependent types we take this to the next level. While most dependently typed systems (e.g. Coq and Agda) aim to be proof assistants rather than programming languages. Idris tries to answer the question how a general purpose programming language with dependent types could look like, it also enables us to produce self contained binaries as well as JavaScript applications today. In this talk I will introduce techniques for programming with dependent types as well as interaction with the programming language itself. Examples will present resource tracking in the type system e.g. tracking file handles and yielding compilation errors on resource leaks, modeling specifications of protocols as types and enforcing them. I argue that functional programming and dependently typed programming languages provide various exciting opportunities to the programmer, including a powerful mental model, compositionality and machine assisted programming through interactive editing capabilities. The presentation software for this talk will be a web application written in Idris which compiles to JavaScript using a compiler backend written by the lecturer.