Programming with Proofs for High-assurance Software

Опубликовано 28 августа 2020, 18:49

Programming critical systems with proofs, a long-standing goal of computer science, is beginning to come within reach of modern programming languages and proof assistants. I provide a brief overview of recent accomplishments in this space, related to work in the F* proof assistant and Project Everest, one of its flagship applications. Programs developed in F* with proofs of correctness are now deployed in wide variety of settings, ranging from Microsoft Windows and Hyper-V, Microsoft Azure, the Linux kernel, Firefox, mbedTLS, and several others production systems.

F* functional programming language: fstar-lang.org
Project Everest: microsoft.com/en-us/research/p...