Hacspec: Executable and Verifiable Specifications for High-Assurance Cryptography

Explore the hacspec domain-specific language for creating succinct, executable, and verifiable specifications in high-assurance cryptography. Learn about the challenges in bridging the gap between formal specifications and implementation, and discover how hacspec addresses the specification problem. Delve into the language's simple call-by-value semantics, linear typing with Rust specificities, and implementation details. Gain insights into the hacspec typechecker, programs, verification backend, and libraries. This 26-minute Rust conference talk, presented by Denis Merigoux, Franziskus Kiefer, and Karthikeyan Bhargavan, offers a comprehensive overview of hacspec's features and its potential impact on high-assurance cryptography development.