Preface

Computers are everywhere, and we rely on software daily. As well as running our desktop and laptop computers, software controls our communications, banking, transport infrastructure, and even our domestic appliances. Even so, it’s considered a fact of life that software is unreliable. If a laptop or mobile phone fails, it’s merely inconvenient and requires a restart (possibly accompanied by cursing over losing the last few minutes of work). If, on the other hand, the software controlling a business-critical application or server fails, significant time and money can be lost. For safety-critical systems, the repercussions could be even worse.

For many years, therefore, computer science researchers have been searching for ways to improve the robustness and safety of software. One approach among many is to use types to describe what a program is supposed to do. In particular, by using dependent types, you describe precise properties of a program. The idea is that if you can express a program’s intention in its type, and the program successfully type-checks, then the program must behave as intended. An important (if ambitious and long-term) goal of the Idris programming language is to make the results of this research accessible to software developers in general, and correspondingly reduce the possibility of critical software failures.