Idris: Programming as a Conversation
Idris is a programming language which encourages “type-driven development”. We believe that to enable the highest levels of productivity, programming should be a conversation between the programmer and the machine. A type represents a formally defined “plan” for a program, which, in type-driven development, is then refined step by step into a complete, working program. The machine then acts as an assistant to the programmer, offering suggestions and synthesis of partial programs. Using a formal specification, Idris can guarantee that resulting programs behave as expected. In this exhibit, I will demonstrate interactive program development in Idris.
Keywords
Programming, Types, Interactive Editing