This is an idea proposed in 2024 as a Cambridge Computer Science Part II project, and is currently being worked on by Max Carroll. It is supervised by Patrick Ferris and Anil Madhavapeddy as part of my Planetary Computing project.
Reasoning about type errors is very difficult, and requires shifting between static and dynamic types. In OCaml, the type checker asserts ill-typedness but provides little in the way of understanding why the type checker inferred such types. These direct error messages are difficult to understand even for experienced programmers working on larger codebases.
This project will explore how to use gradual types to reason more effectively about such ill-typed programs, by introducing more dynamic types to help some users build an intuition about the problem in their code. The intention is to enable a more exploratory approach to constructing well-typed programs.
Some relevant reading: