Flux: Liquid Types for Rust

Explore a groundbreaking conference talk from PLDI 2023 introducing Flux, a novel approach to integrating liquid types with Rust's ownership mechanisms. Delve into how this innovative system enables efficient type-based verification of low-level pointer manipulating programs. Learn about the design of a refined type system for Rust that indexes mutable locations with pure values, leveraging Rust's ownership model to abstract sub-structural reasoning within polymorphic type constructors. Discover how Flux implements this type system as a Rust compiler plug-in, utilizing liquid inference to synthesize loop annotations and complex quantified invariants. Examine the evaluation of Flux through a benchmark suite of vector manipulating programs and parts of a verified secure sandboxing library, comparing its performance to the Prusti verifier. Gain insights into how Flux's liquid typing approach significantly reduces specification lines, verification time, and annotation overhead for lightweight but crucial verification use-cases in Rust programming.

[PLDI'23] Flux: Liquid Types for Rust