Types for Incorrectness

Type systems are an important part of programming because of their ability to give strong guarantees about the freedom of code from certain kinds of defects, such as calling an integer literal as if it were a function, or passing a string to an integer function. However, type systems are conservative: there are always programs that are free from defects and yet fail to pass the typechecker. Such results can be thought of as "false positives" and, in a traditional type system, it's down to the programmer to spend time looking at their type errors and determining which are true bugs and which are false positives. For familiar, mainstream type systems, this is perhaps not too onerous. However, for the cutting-edge type systems developed in programming languages research, which are designed for verifying strong, behavioural properties of programs, the volume of type errors and the effort required to separate those which are true from those that are false positives is prohibitive. The fact that type systems themselves provide no mechanism to distinguish real bugs from false positives is an inherent limitation in the underlying theory. Traditionally, only well-typed programs (those that pass the typechecker) can be assigned types, and well-typed programs don't go wrong. Thus, types in these systems can say nothing about programs with defects, that is (following O'Hearn) program incorrectness. In this project, we develop the theory and practice of type systems for reasoning about program incorrectness, underpinned by Ramsay and Walpole's new framing of type systems as sequent calculi. These two-sided type systems can prove that programs can go wrong, e.g. prove that a given program can be provoked to crash at runtime with a memory fault, or that a program is certain to reveal some private data. A type error in such a system guarantees that there is an issue in the code which can be made manifest at runtime; in other words, there are no false positives. Moreover, the content of the proof can be used to pinpoint the exact execution sequence that will provoke the error, so that programmers can understand why the bug is real. Our aim is to demonstrate that two-sided typing can be a rich foundation for impactful applications in reasoning about incorrectness of higher-order, functional programs. On the foundational side, we will tackle some of the challenging omissions in the nascent theory, such as: sound principles for refutation in the presence of computational effects - especially effects related to message-passing concurrency; the importance of extensionality principles for reasoning about necessity; dependence; and the relationship with incorrectness program logics for first-order, imperative programs. We will test the applicability of the theory by developing a new static analysis tool to automatically detect data-flow violations in large Erlang codebases, such as those of our partners. Such a tool would, for example, pinpoint paths in the code where private data will reach a public sink. Unlike existing tools, its underpinning in two-sided typing can guarantee zero false positives and the provision of detailed information about the diagnosis of issues.