DLS Talk by Nikhil Swamy (Microsoft Research)

Speaker:  Dr. Nikhil Swamy, Microsoft Research, Redmond

Title:  Proof-oriented Programming for Critical Compute Infrastructure

Abstract: 

From the early days of computer science, the potential of mathematical proofs of programs to eradicate large classes of software errors has been widely recognized; however, historically, few practical applications were feasible. The proof techniques were difficult to apply to full-fledged programming languages, and proofs were hard to scale to large programs. But things are changing with recent progress in programming languages and theorem provers, enabling program proofs to be applied to industrial-scale software.

At Microsoft Research, we have been developing a proof-oriented programming language called F*. Proof-oriented programming (PoP) is a paradigm in which programs and their proofs are co-developed in a single framework, enabling both daring programming patterns which, without proofs, would be too risky; conversely, PoP also forces the design and use of robust abstractions that facilitate modular, scalable proofs. We maintain a corpus of proof-oriented code developed in F*, now approaching nearly a million lines of code. Some of this code now runs in the Windows kernel and Azure cloud computing stack, the Linux kernel, Firefox, Python, and several other popular software packages.

While the expertise needed to use a proof-oriented language like F* is still substantial, with continued advances, proof-oriented programming could become the standard way of building the complex, highly optimized programs that underpin society's critical compute infrastructure.

Bio:  Nikhil Swamy is a Senior Principal Researcher in the RiSE group at Microsoft Research, Redmond. His work covers various topics including type systems, program logics, functional programming, and program proof, often applied to build provably secure programs, including web applications, cryptographic software, and low-level systems code. He has been developing F* since before its first commit on GitHub.

Host:  Dr. Alex Summers, UBC Computer Science