Title: Proof-oriented Programming in F*
F* is a proof-oriented programming language that has been used to develop, and deploy, critical software components backed with mathematical proofs of correctness and security. Deployments of programs written and proven in F* include Microsoft Windows Hyper-V, Microsoft Azure, Firefox, Linux, mbedTLS, and several other production systems. In this talk, I will begin with an overview of F* and its applications. I will then talk about our recent work on Steel, a language for programming and proving concurrent programs embedded in F*. Steel is based on a higher-order Concurrent Separation Logic, also derived in F* using a denotation of computations in the effectful semantics of non-deterministically interleaved atomic actions. With Steel we have programmed several verified programs and libraries, including spinlocks, protocol-indexed channel, and various sequential and concurrent data-structures.