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.

Intro
A tale of two worlds
Right now: the specification problem
Bringing the two worlds together
A taste of hacspec
Simple call-by-value semantics with variable context
Linear typing with Rust specificities
Implementation: AST or MIR?
The hacspec typechecker
hacspec programs
Verification backend: F
The hacspec libraries
Conclusion
The hacspec DSL - [7]