Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification

Explore a 30-minute conference talk from ICFP 2023 that delves into innovative language-based techniques for modular program verification. Discover how researchers from Inria and Microsoft Research have developed methods to write and verify high-level, abstract code while maintaining control over compilation and producing zero-overhead, low-level code suitable for mainstream software integration. Learn about the implementation of these techniques within the F* proof assistant and their application in scaling the HACL cryptographic library. Gain insights into a novel case study on the streaming API, demonstrating how this approach captures streaming semantics generically and applies it to multiple use-cases, including improvements to the Python programming language's reference implementation. Understand the impact of these techniques on proof engineer productivity and the potential for enhancing security-critical code verification.