Trustworthy refactoring

When we write programs, we don't always get the code right first time. A function may start off with one purpose that changes to another: the function is now mis-named; we may have chosen a particular way of representing some real-world object as a data structure, but we find that we need to change the representation to make it more general, or adapt to a change in other parts of the organisation. In both cases we need to transform our program, without changing what it already does, even though we change how it does it. This process is called refactoring.

In a program of any size, making the simplest refactoring happen can be complicated. For example, if we rename a commonly used library function this may result in changes in hundreds of files, and making the change can be too costly and error prone to do by hand. For this reason, engineers have built refactoring tools that automate the process of making common refactoring transformations, and these tools can be found for many languages, integrated into programmers' standard workflow (e.g. into the Eclipse IDE for Java). Even so, refactoring tools are used less than might be anticipated: a reason for this is a lack of trust in the tools (see e.g. E Murphy-Hill et al, How We Refactor, and How We Know It, 2012). When we apply a tool, how do we know that it hasn't changed what our program does?

In this project our aim is to make a step change in the way that refactoring tools are built, so that we demonstrably improve the trustworthiness of the way that the tools make the refactorings. For example, in the case of our industrial partners, code changes need to be reviewed by up to three reviewers, and even a straightforward refactoring can give a substantial review overhead. This project will allow reviewers to assure themselves of the safety of changes with substantially less effort.

How will we achieve this? The UK is a world leader in showing how computers can support logical reasoning, either by answering logic questions automatically (SAT/SMT solvers) or by supporting "by hand" proof (proof assistants such as Isabelle and HOL). In this project we will build on our work in the HOL proof assistant to formally verify a compiler for the CakeML language. This infrastructure will help us to build a refactoring tool for CakeML in which we are able to say, in advance, that a particular refactoring - such as renaming - is guaranteed never to break a program.

While this work advances the state of the art for academic computer science, we also want to support the practising engineer, and so in this project we will work closely with Jane Street Capital, a leading user of the OCaml language, to develop a trustworthy refactoring tool for this industrially-relevant language. This tool will provide different levels of assurance from the (strongest) case of a fully formal proof that a refactoring can be trusted to work on all programs, given some pre-conditions, to other, more generally applicable guarantees, that a refactoring applied to a particular program does not change the behaviour of that program.

We will ensure the practicality of the tool by working with industrial partners, Jane Street, and embed one of the researchers in industry for part of the project. The refactorings implemented will be chosen to support development not only in our partners, but also in the wider OCaml developer community, and the tool will be freely available under an open source licence, supporting its sustainability beyond the life of the project.

In providing verified refactorings for CakeML we will go beyond the state of the art for program verification, and in the OCaml development, we will set a new benchmark for building refactoring tools for programming languages in general.

The project brings together CS theory and the practice of programming, as supported by software tools. We see the project as having an impact beyond the purely academic in two complementary directions.

- It will deliver state of the art software development tools, which will deliver a benefit to the software developers in the OCaml programming community.

- The advancements in assurance will have an impact beyond the particular OCaml language on the developers of software tools for other languages and paradigms (and in particular developers of refactoring tools).

Industrial impact

The project will deliver a tool which is intended to become the default refactoring tool for the OCaml developer community. Jane Street is a leading member of that community, with a history of supporting it through open source release of software, such as its versions of the base libraries. They have supported the proposal by promising to contribute 600 hours of effort to the project should it be funded.

In order to consolidate the work done during the project, we have planned a final six month period during which the strands of the project will be integrated together, documented and demonstrated by means of video and other tutorials. We have therefore requested funding for 42 months, allowing 36 months for the theoretical and practical development and the final six for integration activities. This final consolidation period substantially increases the potential range and depth of the industrial impact of the project, for the benefit of the developer community and the wider industrial sector using OCaml.


Mid-term workshop

This approach will be supplemented by a mid-term workshop to be held early in 2018. The workshop will invite leaders in the fields of mechanised (meta)theory and refactoring, allowing us to showcase the achievements of the project thus far and plans for the remainder of the project. The workshop will be supplemented by a tutorial day to give attendees hands-on experience of using the interim results of the project.

User community

For a tool to be of practical value, it needs to be designed with the needs of the user community in mind. We will ensure the relevance of the software to the OCaml developer community by embedding the software development RA with the industrial partner for a total period of six months over the life of the project. This will ensure that the RA will not only be receptive to the requirements of the partner but will also be able to observe for him/herself how such tools are used in practice and suggest functionality for themselves.

Open source development

The software will be documented through a comprehensive website that includes usage information and examples. Take-up of the tool will be promoted through the production of a number of demonstration videos. The software developed will be freely available under open source licence and will be accessible on Github in order to make it as easy as possible for users of the system to themselves become contributors to the software, thus ensuring the longer-term sustainability of the project outcomes.

Video

The project will use online video as a dissemination mechanism to all four of the interested parties: theoreticians, OCaml developers, refactoring tool developers and the wider public. It is planned for the final year of the project to record high production-quality videos, to a total of one hour each, for the four interest groups, and a budget of 10,000 GBP is requested for this.

Researcher training

While a number of skills, such as presentation of work to peers, have been are addressed through the PhD process, the wider task of explaining research to computer scientists and professionals and the general public tend to be more peripheral to the PG researcher. We will address this by requesting £2,000 to support media training for the RAs employed by the grant, in order to enhance their public engagement skills.