权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Programming as Conversation: Type-Driven Development in Action

编程即对话：类型驱动开发的实际应用

基本信息

批准号：
EP/T007265/1
负责人：
Edwin Brady
金额：
$ 46.8万
依托单位：
University of St Andrews
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2020
资助国家：
英国
起止时间：
2020 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FT007265%2F1
关键词：
Programming Conversation Type Driven Development

项目摘要

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.

该项目旨在使用“类型驱动开发”流程来改进程序开发流程。我们相信，为了实现最高水平的生产力，编程应该是程序员和机器之间的对话。在类型驱动的开发中，我们首先给出一个类型作为程序的计划。那么机器就不会被视为拒绝不完整或不正确程序的对手，而是程序员的助手。这种想法的有限形式存在于现代集成开发环境中：当键入“x”时。进入文本缓冲区，环境将显示方法“x”实现。该项目将把这个想法进一步推进。我们不仅可以对部分程序提供反馈，还可以使用类型及其结构来生成程序的重要部分，并指导更复杂组件（例如通信和安全协议）的实现。在开发过程中，程序大部分时间都处于不完整状态，编程行为既涉及实现完整程序所需的步骤，也涉及最终结果。因此，语言实现和工具必须支持编辑过程以及检查和编译最终结果。在这个项目中，我们将基于良好的理论基础，开发必要的工具来支持交互式类型驱动开发。此外，我们将使工具本身可编程：基础本质上将提供一种编程“策略”语言，它将可组合成由类型指导的自动程序构建的复杂方法。我们将始终与业界保持联系，以确保我们开发的技术非常适合商业相关问题。