F⋆ is a dependently typed general-purpose programming language with support for user-defined effects. F⋆ supports Proof-oriented Programming, a paradigm in which programmers co-develop programs and proofs to provide mathematical guarantees about various aspects of program behavior (functional correctness, security properties, etc.). To reason about programs with concurrency and mutable state, a Concurrent Separation Logic (CSL) called Steel has been developed foundationally in F⋆, enabling the use of CSL to reason about dependently typed, effectful F⋆ programs. However, Steel requires the use of various tactics and combinators, making it somewhat difficult to program with.

Recently, leveraging a new framework in F⋆ for embedding domain-specific languages, we have built Pulse, a syntax extension coupled with a custom typechecker for Steel. Pulse enables programs to be developed in a direct, Rust-like imperative syntax. The Pulse typechecker provides extensible proof automation that is backed by a certified correct elaboration into core F⋆. Depending on the libraries they use, well-typed Pulse programs can be extracted to OCaml, to C, or to Rust.

This tutorial aims to provide a hands-on introduction to using Pulse. Attendees will learn Pulse by developing several examples, ranging from first-order sequential programs with mutable state, extracting to Rust and C, to higher-order programs with concurrency using libraries like OCaml 5’s domainslib.