4 ms·

Pulse: Proof-Oriented Programming in Concurrent Separation Logic (Output C/Rust)

• hackingonempty 19d ago
  "Pulse is a new programming language embedded in F*, inheriting many of its features (notably, it is higher order and has dependent types), but with built-in support for programming with mutable state and concurrency, with specifications and proofs in Concurrent Separation Logic." https://github.com/FStarLang/FStar/tree/master/pulse https://github.com/FStarLang/FStar/tree/master/pulse