Programming as Conversation: Type-Driven Development in Action

This project aims to improve the program development process, using a process of "Type-driven Development". We believe that in order to enable the highest levels of productivity, programming should be a conversation between the programmer and the machine. In type-driven development, we begin by giving a type as a plan for a program. Then the machine, rather than being seen as an adversary which rejects incomplete or incorrect programs, is the programmer's assistant. A limited form of this idea exists in modern integrated development environments: when typing "x." into a text buffer, the environment will show with methods "x" implements. This project will take this idea several steps further. Not only can we give feedback on partial programs, we can also use types and their structure to generate significant parts of a program and direct the implementation of more complex components such as communication and security protocols.

During development, programs spend most of their time in an incomplete state, and the act of programming is as much about the steps required to achieve a complete program as it is about the end result. Accordingly, language implementations and tools must support the editing process as well as check and compile the end result. In this project, we will develop the necessary tooling to support interactive type-driven development, based on sound theoretical foundations. Furthermore, we will make the tooling itself programmable: the foundations will essentially give a language of programming "tactics", which will be composable intro sophisticated methods for automatic program construction, directed by the type. We will liaise with industry throughout to ensure that the techniques we develop are well-suited to commercially relevant problems.

In the course of the project, we will make significant advances in the state of the art of dependently typed programming, improving the available tools and developing new libraries and programming idioms. As well as benefitting academic researchers in the field of software verification, it will benefit the wider community of application developers by providing tools to improve programmer productivity.

This project will itself contribute to a longer term vision of fully verified systems infrastructure, thus the public at large will benefit from techniques which enable the development of stable, robust software at reduced cost. We are collaborating with companies and research institutions who may make use of the results of this project, In particular, we will be working with PIK, the Potsdam Institute for Climate Impact Research, who have been using Idris for several years for formalising economic models related to climate change, and who will benefit from the increased productivity offered by this project. We are also working with developers at Facebook, who develop large scale systems in Haskell, another language with a sophisticated type system which will benefit from type-driven interactive programming techniques. Finally, our contacts at Galois, Inc, in Portland, Oregon, are using Haskell and domain specific language technology to build tools for guaranteed confidentiality including secure voting systems. By liasing with these companies, we will be able to direct the research towards supporting socially and commercially important problems. We will also liaise with Microsoft Research, where researchers are developing GHC (the de facto standard Haskell compiler), in order to make our techniques usable by Haskell programmers, as well as in our own Idris compiler.

The project will involve development of a new, self-hosted, version of the Idris programming language (http://idris-lang.org). As with all code released as part of the Idris system so far, everything produced during the project will be released under an Open Source licence, and made available via GitHub (http://www.github.com/) and the project web site. Throughout the project we will hold a series of open "Idris Developer Meetings" (following an earlier series in 2013-2015) to allow project contributors and others to work closely with the project team.

To help make the results of the project accessible to a wider audience of application developers (the most likely primary users of the project's results) we will continue to present workshops and tutorials alongside developer conferences such as Strange Loop, Code Mesh, and others. These workshops will give developers a hands-on opportunity to try type-driven development tools, with close support from the project team. These workshops will be made more effective with the support of the recently published book "Type-driven Development with Idris", which sets out some of the ideas which are the foundation of this project.