University of Oxford Logo University of OxfordProfessional Master’s programme - Home
ROP

Robust Programming

This course is about writing correct code: specification of what it means for a program to be correct; post hoc verification that a program does indeed satisfy its specification; and correct-by-construction derivation of a program directly from a specification. It teaches techniques for developing programs whose form evidently matches their intended function. This is especially important when we are faced with AI techniques that can churn out code with little thought.

As the late Tony Hoare, the founder of this programme, wrote in his Turing Award Lecture in 1980: "There are two ways of constructing a software design. One way is to make it so simple that there are obviously no deficiencies. The other way is to make it so complicated that there are no obvious deficiencies." If you aspire to writing programs with obviously no deficiencies, this course is for you.

Course dates

25th January 2027Oxford University Department of Computer Science - Held in the Department16 places remaining.
24th January 2028Oxford University Department of Computer Science - Held in the Department18 places remaining.

Objectives

At the end of the course, you will be able to:

  • explain some of the many ways in which programs may be incorrect;
  • define what ‘correctness’ means, and how it may be demonstrated;
  • understand a variety of approaches for specifying and verifying correctness;
  • select among techniques for deriving code that is correct by construction;
  • apply those techniques to concrete examples;
  • appreciate when an aspiration to correctness is reasonable, and when it is not.

Contents

Introduction:
motivating examples; the problem with testing; specification, verification, and derivation; programming as a mathematical activity; formal methods
Hoare logic:
design by contract; assertions; defensive programming; Liskov substitutivity; pre- and post-conditions; invariants; weakest precondition calculus; refinement calculus; separation logic; using Dafny
Modelling and refinement:
relations (a recap of Z); state-based models; model finding; model checking; data abstraction; data refinement and simulation; using Alloy
Type systems:
ownership types; Rust's borrow checker; region typing; polymorphism, and free theorems; dimension and unit checking; shape checking; resource types; dependent types; Curry--Howard Correspondence; type-driven development; gradual typing; using Agda
Tool support:
automated verification; gstatic analysis; program synthesis; proof assistants; overview of some modern tools
Limitations:
capturing requirements; understanding specifications; managing complexity; communication; offputting theory

Requirements

The course will assume competence in programming, in any programming language. It is designed to complement SEM and SBM, which are recommended, but not required; if you are taking them too, then ideally you would take SEM first, but SBM and ROP could be in either order. Some of the material builds on ideas from FPR and ALG, but any dependencies will be reviewed in the course; if you are doing either of those as well, it doesn't matter whether you take them before or after ROP.

Reading list