hacspec is a specification language for crypto primitives, protocols, and more. It is a subset of the Rust programming language, focused on functional programming and it avoids the use of mutable state as much as possible.

This book gives an overview of:

For a quick introduction you can also check out these slides from April 2021. An in-depth technical report is also available, and serves as a reference for the language formalization.