| Title | : | Proof-oriented Programming for Critical Compute Infrastructure |
| Speaker | : | Nikhil Swamy (Microsoft Research Redmond) |
| Details | : | Mon, 9 Oct, 2023 4:00 PM @ CSB 25 |
| 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. |
