Does Rust SPARK Joy? Safe Bindings from Rust to SPARK, Applied to the BBQueue Library

Explore the challenges and potential benefits of maintaining compile-time safety guarantees across language boundaries in a 29-minute video presentation from the FTSCS 2023 conference. Delve into a study examining the integration of Rust and SPARK, two memory-safe programming languages, through Foreign Function Interface (FFI). Learn how researchers applied their method to the BBQueue circular buffer library, which features complex ownership hand-over patterns. Discover the findings on preserving inherent consistency and safety features when establishing library interfaces between Rust and SPARK, and understand the precautions necessary at the FFI boundary to prevent potential vulnerabilities. Gain insights into the implications for safety-critical code and embedded systems development from experts at KTH Royal Institute of Technology, Ferrous Systems, and AdaCore.